More debugging of handling of open constrs with typeclasses:

avoid trying to resolve classes early in open constr arguments for Ltac,
the tactics themselves should do whatever's appropriate with the constraints.


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

1 files changed, 14 insertions, 13 deletions

diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index c114a922c..83594466e 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -696,12 +696,13 @@ module Pretyping_F (Coercion : Coercion.S) = struct
       | IsType ->
 	  (pretype_type empty_valcon env evdref lvar c).utj_val in
     let evd,_ = consider_remaining_unif_problems env !evdref in
-      evdref := evd; c'
+      evdref := evd; 
+      nf_isevar !evdref c'
 	
   let pretype_gen evdref env lvar kind c =
     let c = pretype_gen_aux evdref env lvar kind c in
       evdref := Typeclasses.resolve_typeclasses ~onlyargs:true ~fail:false env !evdref;
-      nf_evar (evars_of !evdref) c
+      nf_isevar !evdref c
 	
   (* TODO: comment faire remonter l'information si le typage a resolu des
      variables du sigma original. il faudrait que la fonction de typage
@@ -730,7 +731,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct
 
   let ise_pretype_gen fail_evar sigma env lvar kind c =
     let evdref = ref (Evd.create_evar_defs sigma) in
-    let c = pretype_gen evdref env lvar kind c in
+    let c = pretype_gen_aux evdref env lvar kind c in
     let evd,_ = consider_remaining_unif_problems env !evdref in
       if fail_evar then 
 	let evd = Typeclasses.resolve_typeclasses ~onlyargs:false ~fail:true env evd in
@@ -755,17 +756,17 @@ module Pretyping_F (Coercion : Coercion.S) = struct
       
   let understand_tcc_evars evdref env kind c =
     pretype_gen evdref env ([],[]) kind c
-
+      
   let understand_tcc ?(resolve_classes=true) sigma env ?expected_type:exptyp c =
     let evd, t =
-      if resolve_classes then
-	ise_pretype_gen false sigma env ([],[]) (OfType exptyp) c 
-      else
-	let evdref = ref (Evd.create_evar_defs sigma) in
-	let c = pretype_gen_aux evdref env ([],[]) (OfType exptyp) c in
-	  !evdref, nf_isevar !evdref c
-    in
-    Evd.evars_of evd, t
+      let evdref = ref (Evd.create_evar_defs sigma) in
+      let c = 
+	if resolve_classes then
+	  pretype_gen evdref env ([],[]) (OfType exptyp) c 
+	else
+	  pretype_gen_aux evdref env ([],[]) (OfType exptyp) c
+      in !evdref, c
+    in Evd.evars_of evd, t
 end
-
+  
 module Default : S = Pretyping_F(Coercion.Default)