diff options
| author |  msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-11-05 20:32:10 +0000 |
|---|---|---|
| committer | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-11-05 20:32:10 +0000 |
| commit | 1785ae696ca884ddd70e4b87fd1d425b06e64abe (patch) | |
| tree | 8bcb6099c1dec80d67dece39ede9200aebfe3d8f /theories | |
| parent | 5438bfe94fd1cb0d22de54df53bd0e09328a90a4 (diff) | |
Fix in the unification algorithm using evars: unify types of evar
instances and the corresponding evar's type if it contains existentials
to avoid dangling evars. No noticeable performance impact (at least on the
stdlib). Subsumes (and fixes) the (broken) fix in unification.ml that was
previously patched by M. Puech.
Improve error messages related to existential variables and type
classes.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11543 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories')
0 files changed, 0 insertions, 0 deletions