| Mon, 06 Jun 2011 20:36:35 +0200 | blanchet | tuning | changeset | files |
| Mon, 06 Jun 2011 20:36:35 +0200 | blanchet | gracefully handle the case where a constant is partially or not instantiated at all, as may happen when reconstructing Metis proofs for polymorphic type encodings | changeset | files |
| Mon, 06 Jun 2011 20:36:35 +0200 | blanchet | temporarily document "metisX" | changeset | files |
| Mon, 06 Jun 2011 20:36:34 +0200 | blanchet | use "metisX" as fallback, since it's much faster than "metisFT" | changeset | files |
| Mon, 06 Jun 2011 20:36:34 +0200 | blanchet | temporarily added "MetisX" as reconstructor and minimizer | changeset | files |
| Mon, 06 Jun 2011 20:36:34 +0200 | blanchet | ensured that the logic for "explicit_apply = smart" also works on CNF (i.e. new Metis) | changeset | files |
| Mon, 06 Jun 2011 20:36:34 +0200 | blanchet | show what failed to play | changeset | files |