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/typeclasses.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/typeclasses.mli')
| -rw-r--r-- | pretyping/typeclasses.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli index c437d9eab2..1f1bdb4ffc 100644 --- a/pretyping/typeclasses.mli +++ b/pretyping/typeclasses.mli @@ -30,7 +30,7 @@ type typeclass = { (* Context in which the definitions are typed. Includes both typeclass parameters and superclasses. The boolean indicates if the typeclass argument is a direct superclass and the global reference - gives a direct link to the class itselft. *) + gives a direct link to the class itself. *) cl_context : (global_reference * bool) option list * rel_context; (* Context of definitions and properties on defs, will not be shared *) |