Fri, 29 Oct 2010 12:49:05 +0200 | blanchet | restructure Skolemization code slightly | changeset | files |
Fri, 29 Oct 2010 12:49:05 +0200 | blanchet | ensure that MESON correctly preserves the name of variables (needed by the new Skolemizer) | changeset | files |
Fri, 29 Oct 2010 12:49:05 +0200 | blanchet | more work on new Skolemizer without Hilbert_Choice | changeset | files |
Fri, 29 Oct 2010 12:49:05 +0200 | blanchet | fix cluster numbering in the absense of Hilbert_Choice (reverts acde1b606b0e, effectively reintroducing most of 0bfaaa81fc62) | changeset | files |
Fri, 29 Oct 2010 12:49:05 +0200 | blanchet | prevent type errors because of inconsistent skolem Var types by giving fresh indices to Skolems | changeset | files |
Fri, 29 Oct 2010 12:49:05 +0200 | blanchet | make handling of parameters more robust, by querying the goal | changeset | files |