- Remove create_evar_defs

- Be careful with consider_remaining_unif_problems: it might instantiate an evar, including the current goal!

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

4 files changed, 10 insertions, 6 deletions

diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index 4dfe035007..64c5c5a9e4 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -171,7 +171,10 @@ and e_my_find_search db_list local_db hdc concl =
               tclTHEN (with_prods nprods (term,cl) (unify_e_resolve flags))
 		(e_trivial_fail_db db_list local_db)
 	  | Unfold_nth c -> tclWEAK_PROGRESS (unfold_in_concl [all_occurrences,c])
-	  | Extern tacast -> conclPattern concl p tacast
+	  | Extern tacast -> 
+	    tclTHEN
+	      (fun gl -> Refiner.tclEVARS (mark_unresolvables (project gl)) gl)
+	      (conclPattern concl p tacast)
       in
 	match t with
 	| Extern _ -> (tac,b,true,lazy (pr_autotactic t))
diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4
index 4d8fc0e441..a01799b181 100644
--- a/tactics/rewrite.ml4
+++ b/tactics/rewrite.ml4
@@ -1074,7 +1074,7 @@ let cl_rewrite_clause_aux ?(abs=None) strat env avoid sigma concl is_hyp : resul
       | None -> (sort, inverse sort impl)
       | Some _ -> (sort, impl)
   in
-  let evars = (create_evar_defs sigma, Evd.empty) in
+  let evars = (sigma, Evd.empty) in
   let eq = apply_strategy strat env avoid concl (Some cstr) evars in
     match eq with
     | Some (Some (p, evars, car, oldt, newt)) ->
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 735de9371c..b33942b0cd 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -1253,7 +1253,8 @@ let solvable_by_tactic env evi (ev,args) src =
 
 let solve_remaining_evars fail_evar use_classes env initial_sigma evd c =
   let evdref =
-    if use_classes then ref (Typeclasses.resolve_typeclasses ~fail:true env evd)
+    if use_classes then 
+      ref (Typeclasses.resolve_typeclasses ~split:true ~fail:fail_evar env evd)
     else ref evd in
   let rec proc_rec c =
     let c = Reductionops.whd_evar !evdref c in
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 4e6a293c98..d960908337 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -590,7 +590,7 @@ let resolve_classes gl =
   let env = pf_env gl and evd = project gl in
     if Evd.is_empty evd then tclIDTAC gl
     else
-      let evd' = Typeclasses.resolve_typeclasses env (Evd.create_evar_defs evd) in
+      let evd' = Typeclasses.resolve_typeclasses env evd in
 	(tclTHEN (tclEVARS evd') tclNORMEVAR) gl
 
 (**************************)
@@ -2391,7 +2391,7 @@ let abstract_generalize ?(generalize_vars=true) ?(force_dep=false) id gl =
 let specialize_eqs id gl =
   let env = pf_env gl in
   let ty = pf_get_hyp_typ gl id in
-  let evars = ref (create_evar_defs (project gl)) in
+  let evars = ref (project gl) in
   let unif env evars c1 c2 = Evarconv.e_conv env evars c2 c1 in
   let rec aux in_eqs ctx acc ty =
     match kind_of_term ty with
@@ -3440,6 +3440,6 @@ let unify ?(state=full_transparent_state) x y gl =
 	modulo_conv_on_closed_terms = Some state}
     in
     let evd = w_unify false (pf_env gl) Reduction.CONV
-      ~flags x y (Evd.create_evar_defs (project gl))
+      ~flags x y (project gl)
     in tclEVARS evd gl
   with _ -> tclFAIL 0 (str"Not unifiable") gl