| Tue, 31 May 2011 16:38:36 +0200 |
blanchet |
no need for type arguments with "xxx_tags_heavy" type system
|
changeset |
files
|
| Tue, 31 May 2011 16:38:36 +0200 |
blanchet |
use ":" for type information (looks good in Metis's output) and handle it in new path finder
|
changeset |
files
|
| Tue, 31 May 2011 16:38:36 +0200 |
blanchet |
tuned name
|
changeset |
files
|
| Tue, 31 May 2011 16:38:36 +0200 |
blanchet |
tuned name
|
changeset |
files
|
| Tue, 31 May 2011 16:38:36 +0200 |
blanchet |
make "prepare_atp_problem" more robust w.r.t. choice of type system
|
changeset |
files
|
| Tue, 31 May 2011 16:38:36 +0200 |
blanchet |
parse optional type system specification
|
changeset |
files
|
| Tue, 31 May 2011 16:38:36 +0200 |
blanchet |
tuning
|
changeset |
files
|
| Tue, 31 May 2011 16:38:36 +0200 |
blanchet |
proper handling of type variable classes in new Metis
|
changeset |
files
|
| Tue, 31 May 2011 16:38:36 +0200 |
blanchet |
fixed recursive call in new path finder and (untested:) handle hAPP
|
changeset |
files
|
| Tue, 31 May 2011 16:38:36 +0200 |
blanchet |
don't preprocess twice
|
changeset |
files
|
| Tue, 31 May 2011 16:38:36 +0200 |
blanchet |
more robust and simpler adjustment computation
|
changeset |
files
|
| Tue, 31 May 2011 16:38:36 +0200 |
blanchet |
more work on new Metis
|
changeset |
files
|
| Tue, 31 May 2011 16:38:36 +0200 |
blanchet |
tuning
|
changeset |
files
|
| Tue, 31 May 2011 16:38:36 +0200 |
blanchet |
more work on new metis that exploits the powerful new type encodings
|
changeset |
files
|
| Tue, 31 May 2011 16:38:36 +0200 |
blanchet |
tuning
|
changeset |
files
|
| Tue, 31 May 2011 16:38:36 +0200 |
blanchet |
removed obscure option
|
changeset |
files
|
| Tue, 31 May 2011 16:38:36 +0200 |
blanchet |
added "metisX" syntax (temporary)
|
changeset |
files
|
| Tue, 31 May 2011 16:38:36 +0200 |
blanchet |
compile
|
changeset |
files
|
| Tue, 31 May 2011 16:38:36 +0200 |
blanchet |
added new metis mode, with no implementation yet
|
changeset |
files
|
| Tue, 31 May 2011 16:38:36 +0200 |
blanchet |
tuning
|
changeset |
files
|
| Tue, 31 May 2011 16:38:36 +0200 |
blanchet |
first step in sharing more code between ATP and Metis translation
|
changeset |
files
|
| Tue, 31 May 2011 11:21:47 +0200 |
krauss |
more precise authorship, reflecting my own ignorance and hg annotate
|
changeset |
files
|
| Tue, 31 May 2011 11:16:52 +0200 |
krauss |
generate raw induction rule as instance of generic rule with careful treatment of currying
|
changeset |
files
|
| Tue, 31 May 2011 11:16:34 +0200 |
krauss |
generic fixpoint induction (with explicit curry/uncurry predicates) and instance for option type
|
changeset |
files
|