Fixes incorrect handling of existing existentials variables in

 typeclass code.


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11047 85f007b7-540e-0410-9357-904b9bb8a0f7

3 files changed, 17 insertions, 7 deletions

diff --git a/contrib/subtac/subtac_classes.ml b/contrib/subtac/subtac_classes.ml
index 3ebc3bb5c5..67b3adede3 100644
--- a/contrib/subtac/subtac_classes.ml
+++ b/contrib/subtac/subtac_classes.ml
@@ -157,8 +157,7 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(on_free_vars=Class
   in
   let env' = Classes.push_named_context ctx' env in
   isevars := Evarutil.nf_evar_defs !isevars;
-  let sigma = Evd.evars_of !isevars in
-  isevars := resolve_typeclasses ~onlyargs:false ~fail:true env' sigma !isevars;
+  isevars := resolve_typeclasses ~onlyargs:false ~fail:true env' !isevars;
   let sigma = Evd.evars_of !isevars in
   let substctx = Typeclasses.nf_substitution sigma subst in
   let subst, _propsctx = 
diff --git a/contrib/subtac/subtac_pretyping.ml b/contrib/subtac/subtac_pretyping.ml
index 2118dfbdda..24066d860e 100644
--- a/contrib/subtac/subtac_pretyping.ml
+++ b/contrib/subtac/subtac_pretyping.ml
@@ -73,7 +73,7 @@ let interp env isevars c tycon =
   let _ = isevars := Evarutil.nf_evar_defs !isevars in
   let evd,_ = consider_remaining_unif_problems env !isevars in
 (*   let unevd = undefined_evars evd in *)
-  let unevd' = Typeclasses.resolve_typeclasses ~onlyargs:true ~fail:false env (Evd.evars_of evd) evd in
+  let unevd' = Typeclasses.resolve_typeclasses ~onlyargs:true ~fail:false env evd in
   let evm = evars_of unevd' in
     isevars := unevd';
     nf_evar evm j.uj_val, nf_evar evm j.uj_type
diff --git a/contrib/subtac/subtac_pretyping_F.ml b/contrib/subtac/subtac_pretyping_F.ml
index 32aa3e4131..808039de6b 100644
--- a/contrib/subtac/subtac_pretyping_F.ml
+++ b/contrib/subtac/subtac_pretyping_F.ml
@@ -550,7 +550,7 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
 		  error_unexpected_type_loc
                     (loc_of_rawconstr c) env (evars_of !isevars) tj.utj_val v
 
-  let pretype_gen isevars env lvar kind c =
+  let pretype_gen_aux isevars env lvar kind c =
     let c' = match kind with
       | OfType exptyp ->
 	  let tycon = match exptyp with None -> empty_tycon | Some t -> mk_tycon t in
@@ -558,10 +558,14 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
       | IsType ->
 	  (pretype_type empty_valcon env isevars lvar c).utj_val in
     let evd,_ = consider_remaining_unif_problems env !isevars in
-    let evd = Typeclasses.resolve_typeclasses ~onlyargs:true ~fail:false env (evars_of evd) evd in
       isevars:=evd;
       nf_evar (evars_of !isevars) c'
 
+  let pretype_gen isevars env lvar kind c =
+    let c = pretype_gen_aux isevars env lvar kind c in
+      isevars := Typeclasses.resolve_typeclasses ~onlyargs:true ~fail:false env !isevars;
+      nf_evar (evars_of !isevars) c
+
   (* TODO: comment faire remonter l'information si le typage a resolu des
      variables du sigma original. il faudrait que la fonction de typage
      retourne aussi le nouveau sigma...
@@ -609,8 +613,15 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
   let understand_tcc_evars evdref env kind c =
     pretype_gen evdref env ([],[]) kind c 
 
-  let understand_tcc sigma env ?expected_type:exptyp c =
-    let ev, t = ise_pretype_gen false sigma env ([],[]) (OfType exptyp) c in
+  let understand_tcc ?(resolve_classes=true) sigma env ?expected_type:exptyp c =
+    let ev, t = 
+      if resolve_classes then
+	ise_pretype_gen false sigma env ([],[]) (OfType exptyp) c 
+      else
+	let isevars = ref (Evd.create_evar_defs sigma) in
+	let c = pretype_gen_aux isevars env ([],[]) (OfType exptyp) c in
+	  !isevars, c
+    in
       Evd.evars_of ev, t
 end