diff options
| author |  msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-06-09 15:34:47 +0000 |
|---|---|---|
| committer | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-06-09 15:34:47 +0000 |
| commit | d9fa2c0a9d6b10fe592dd6fb634d8ddc92b4e2ed (patch) | |
| tree | 1979ead2112dae9d4f829074094dd02d179a1406 /Makefile.common | |
| parent | da8f274d07acc80f95928979730bd390984aaf1b (diff) | |
More fixes in pruning/restriction of evars during unification.
- Do not allow to filter variables that appear in the conclusion of an evar.
- Do not attempt to restrict evars based on a substitution that does not contain only evars
(fall back to the pattern fragment and do not lose solutions).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14174 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'Makefile.common')
0 files changed, 0 insertions, 0 deletions