diff options
| author | msozeau | 2008-11-05 20:32:10 +0000 |
|---|---|---|
| committer | msozeau | 2008-11-05 20:32:10 +0000 |
| commit | 1785ae696ca884ddd70e4b87fd1d425b06e64abe (patch) | |
| tree | 8bcb6099c1dec80d67dece39ede9200aebfe3d8f /pretyping/termops.mli | |
| 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 'pretyping/termops.mli')
| -rw-r--r-- | pretyping/termops.mli | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/pretyping/termops.mli b/pretyping/termops.mli index 92c0a78d48..f5f1a459f4 100644 --- a/pretyping/termops.mli +++ b/pretyping/termops.mli @@ -93,6 +93,7 @@ val strip_head_cast : constr -> constr exception Occur val occur_meta : types -> bool val occur_existential : types -> bool +val occur_meta_or_existential : types -> bool val occur_const : constant -> types -> bool val occur_evar : existential_key -> types -> bool val occur_in_global : env -> identifier -> constr -> unit |