From 1785ae696ca884ddd70e4b87fd1d425b06e64abe Mon Sep 17 00:00:00 2001
From: msozeau
Date: Wed, 5 Nov 2008 20:32:10 +0000
Subject: 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
---
 pretyping/typeclasses.mli | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'pretyping/typeclasses.mli')

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 *)
-- 
cgit v1.2.3