| Thu, 31 Mar 2011 14:02:03 +0200 | boehmes | provide a flag controlling whether all provided facts should be instantiated, possibly inventing new types (which does not work well with Sledgehammer) | changeset | files |
| Thu, 31 Mar 2011 11:16:54 +0200 | blanchet | start monomorphization process with subgoal, not entire goal, to avoid needless instances (and only print monomorphization messages in debug mode) | changeset | files |
| Thu, 31 Mar 2011 11:16:53 +0200 | blanchet | temporary workaround: filter out spurious monomorphic instances | changeset | files |