| Fri, 18 Nov 2011 11:47:12 +0100 |
blanchet |
move eta-contraction to before translation to Metis, to ensure everything stays in sync
|
file |
diff |
annotate
|
| Fri, 18 Nov 2011 11:47:12 +0100 |
blanchet |
avoid that var names get changed by resolution in Metis lambda-lifting
|
file |
diff |
annotate
|
| Fri, 18 Nov 2011 11:47:12 +0100 |
blanchet |
avoid spurious messages in "lam_lifting" mode
|
file |
diff |
annotate
|
| Fri, 18 Nov 2011 11:47:12 +0100 |
blanchet |
eta-contract to avoid needless "lambda" wrappers
|
file |
diff |
annotate
|
| Wed, 16 Nov 2011 17:06:14 +0100 |
blanchet |
give each time slice its own lambda translation
|
file |
diff |
annotate
|
| Wed, 16 Nov 2011 13:22:36 +0100 |
blanchet |
make metis reconstruction handling more flexible
|
file |
diff |
annotate
|
| Wed, 16 Nov 2011 09:42:27 +0100 |
blanchet |
parse lambda translation option in Metis
|
file |
diff |
annotate
|
| Tue, 15 Nov 2011 22:20:58 +0100 |
blanchet |
rename the lambda translation schemes, so that they are understandable out of context
|
file |
diff |
annotate
|
| Tue, 15 Nov 2011 22:15:51 +0100 |
blanchet |
rename configuration option to more reasonable length
|
file |
diff |
annotate
|
| Tue, 15 Nov 2011 22:13:39 +0100 |
blanchet |
continued implementation of lambda-lifting in Metis
|
file |
diff |
annotate
|
| Tue, 15 Nov 2011 22:13:39 +0100 |
blanchet |
started implementing lambda-lifting in Metis
|
file |
diff |
annotate
|
| Thu, 22 Sep 2011 16:30:47 +0200 |
blanchet |
better type reconstruction -- prevents ill-instantiations in proof replay
|
file |
diff |
annotate
|
| Thu, 15 Sep 2011 10:57:40 +0200 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Wed, 07 Sep 2011 09:10:41 +0200 |
blanchet |
rationalize uniform encodings
|
file |
diff |
annotate
|
| Fri, 02 Sep 2011 14:43:20 +0200 |
blanchet |
renamed "Metis_Tactics" to "Metis_Tactic", now that there is only one Metis tactic ("metisFT" is legacy)
|
file |
diff |
annotate
| base
|