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

3 files changed, 24 insertions, 16 deletions

diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index c114a922c0..83594466eb 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)
diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml
index f368ed3791..b1dc7c8961 100644
--- a/proofs/clenvtac.ml
+++ b/proofs/clenvtac.ml
@@ -77,8 +77,11 @@ let clenv_pose_dependent_evars with_evars clenv =
 let clenv_refine with_evars clenv gls =
   let clenv = clenv_expand_metas clenv in
   let clenv = clenv_pose_dependent_evars with_evars clenv in
+  let evd' = Typeclasses.resolve_typeclasses ~fail:(not with_evars)
+    clenv.env clenv.evd 
+  in
   tclTHEN
-    (tclEVARS (evars_of clenv.evd)) 
+    (tclEVARS (evars_of evd')) 
     (refine (clenv_value_cast_meta clenv))
     gls
 
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index aa5aaed3b7..063f387ac3 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -1438,7 +1438,7 @@ let solve_remaining_evars env initial_sigma evd c =
 	      Pretype_errors.error_unsolvable_implicit loc env sigma evi src None)
       | _ -> map_constr proc_rec c      
   in
-  proc_rec c
+  proc_rec (Evarutil.nf_isevar !evdref c)
 
 let interp_gen kind ist sigma env (c,ce) =
   let (ltacvars,unbndltacvars as vars) = constr_list ist env in
@@ -1466,6 +1466,10 @@ let interp_open_constr ccl ist sigma env cc =
   let evd,c = interp_gen (OfType ccl) ist sigma env cc in
   (evars_of evd,c)
 
+let interp_open_type ccl ist sigma env cc =
+  let evd,c = interp_gen IsType ist sigma env cc in
+  (evars_of evd,c)
+
 let interp_constr = interp_econstr (OfType None)
 
 let interp_type = interp_econstr IsType
@@ -2200,7 +2204,7 @@ and interp_atomic ist gl = function
       h_mutual_cofix b (interp_fresh_ident ist gl id) (List.map f l)
   | TacCut c -> h_cut (pf_interp_type ist gl c)
   | TacAssert (t,ipat,c) ->
-      let c = (if t=None then pf_interp_constr else pf_interp_type) ist gl c in
+      let c = (if t=None then interp_constr else interp_type) ist (project gl) (pf_env gl) c in
       abstract_tactic (TacAssert (t,ipat,inj_open c))
         (Tactics.forward (Option.map (interp_tactic ist) t)
 	  (interp_intro_pattern ist gl ipat) c)