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.ml | |
| 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.ml')
| -rw-r--r-- | pretyping/termops.ml | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/pretyping/termops.ml b/pretyping/termops.ml index aa6cc297b3..99252ce653 100644 --- a/pretyping/termops.ml +++ b/pretyping/termops.ml @@ -473,6 +473,13 @@ let occur_existential c = | _ -> iter_constr occrec c in try occrec c; false with Occur -> true +let occur_meta_or_existential c = + let rec occrec c = match kind_of_term c with + | Evar _ -> raise Occur + | Meta _ -> raise Occur + | _ -> iter_constr occrec c + in try occrec c; false with Occur -> true + let occur_const s c = let rec occur_rec c = match kind_of_term c with | Const sp when sp=s -> raise Occur |