| Thu, 14 Jul 2011 15:14:38 +0200 | blanchet | fix subtle type inference bug in Metis -- different occurrences of the same Skolem might need to be typed differently, using paramify_vars overconstraints the typing problem | changeset | files |
| Thu, 14 Jul 2011 15:14:38 +0200 | blanchet | use monomorphic encoding as fallback, since they tend to produce fewer type errors | changeset | files |
| Thu, 14 Jul 2011 15:14:38 +0200 | blanchet | don't generate Waldmeister problems with only a conjecture, since it makes it crash sometimes | changeset | files |
| Thu, 14 Jul 2011 15:14:37 +0200 | blanchet | clearer unsound message | changeset | files |
| Thu, 14 Jul 2011 15:14:37 +0200 | blanchet | clarify fine soundness point | changeset | files |
| Thu, 14 Jul 2011 15:14:37 +0200 | blanchet | always unfold "Let"s is Sledgehammer, Metis, and MESON | changeset | files |
| Thu, 14 Jul 2011 15:14:37 +0200 | blanchet | unbreak Nitrox's parsing | changeset | files |