Fix looping class resolution bug discovered by B. Aydemir and use the

right unification flags for exact hints in eauto (may break a lot of 
things by succeeding much more often).


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

4 files changed, 16 insertions, 14 deletions

diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml
index 50529d32a7..62518eaf74 100644
--- a/proofs/clenvtac.ml
+++ b/proofs/clenvtac.ml
@@ -72,10 +72,12 @@ let clenv_pose_dependent_evars with_evars clenv =
   clenv_pose_metas_as_evars clenv dep_mvs
 
 
-let clenv_refine with_evars clenv gls =
+let clenv_refine with_evars ?(with_classes=true) clenv gls =
   let clenv = clenv_pose_dependent_evars with_evars clenv in
-  let evd' = Typeclasses.resolve_typeclasses ~fail:(not with_evars)
-    clenv.env clenv.evd 
+  let evd' = 
+    if with_classes then 
+      Typeclasses.resolve_typeclasses ~fail:(not with_evars) clenv.env clenv.evd 
+    else clenv.evd
   in
   tclTHEN
     (tclEVARS (evars_of evd')) 
@@ -109,11 +111,11 @@ let fail_quick_unif_flags = {
 }
 
 (* let unifyTerms m n = walking (fun wc -> fst (w_Unify CONV m n [] wc)) *)
-let unifyTerms m n gls = 
+let unifyTerms ?(flags=fail_quick_unif_flags) m n gls = 
   let env = pf_env gls in
   let evd = create_goal_evar_defs (project gls) in
-  let evd' = w_unify false env CONV ~flags:fail_quick_unif_flags m n evd in
+  let evd' = w_unify false env CONV ~flags m n evd in
   tclIDTAC {it = gls.it; sigma = evars_of evd'}
 
-let unify m gls =
-  let n = pf_concl gls in unifyTerms m n gls
+let unify ?(flags=fail_quick_unif_flags) m gls =
+  let n = pf_concl gls in unifyTerms ~flags m n gls
diff --git a/proofs/clenvtac.mli b/proofs/clenvtac.mli
index 4dd59fcf65..96fb262a17 100644
--- a/proofs/clenvtac.mli
+++ b/proofs/clenvtac.mli
@@ -21,8 +21,8 @@ open Unification
 (*i*)
 
 (* Tactics *)
-val unify : constr -> tactic
-val clenv_refine : evars_flag -> clausenv -> tactic
+val unify : ?flags:unify_flags -> constr -> tactic
+val clenv_refine : evars_flag -> ?with_classes:bool -> clausenv -> tactic
 val res_pf : clausenv -> ?with_evars:evars_flag -> ?allow_K:bool -> ?flags:unify_flags -> tactic
 val elim_res_pf_THEN_i : clausenv -> (clausenv -> tactic array) -> tactic
 
diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index 8700019ede..001ae03158 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -88,13 +88,13 @@ let unify_e_resolve flags (c,clenv) gls =
   let clenv' = connect_clenv gls clenv in
   let clenv' = clenv_unique_resolver false ~flags clenv' gls 
   in
-    Clenvtac.clenv_refine true clenv' gls
+    Clenvtac.clenv_refine true ~with_classes:false clenv' gls
       
 let unify_resolve flags (c,clenv) gls = 
   let clenv' = connect_clenv gls clenv in
   let clenv' = clenv_unique_resolver false ~flags clenv' gls 
   in
-    Clenvtac.clenv_refine false clenv' gls
+    Clenvtac.clenv_refine false ~with_classes:false clenv' gls
 
 let flags_of_state st =
   {auto_unif_flags with 
diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4
index dcff753315..ea50107ceb 100644
--- a/tactics/eauto.ml4
+++ b/tactics/eauto.ml4
@@ -31,9 +31,9 @@ open Auto
 open Rawterm
 open Hiddentac
 
-let e_give_exact c gl = let t1 = (pf_type_of gl c) and t2 = pf_concl gl in 
+let e_give_exact ?(flags=Unification.default_unify_flags) c gl = let t1 = (pf_type_of gl c) and t2 = pf_concl gl in 
   if occur_existential t1 or occur_existential t2 then 
-     tclTHEN (Clenvtac.unify t1) (exact_check c) gl
+     tclTHEN (Clenvtac.unify ~flags t1) (exact_check c) gl
   else exact_check c gl
 
 let assumption id = e_give_exact (mkVar id)
@@ -173,7 +173,7 @@ and e_my_find_search_delta db_list local_db hdc concl =
 	 match t with
 	   | Res_pf (term,cl) -> unify_resolve st (term,cl)
 	   | ERes_pf (term,cl) -> unify_e_resolve st (term,cl)
-	   | Give_exact (c) -> e_give_exact_constr c
+	   | Give_exact (c) -> e_give_exact ~flags:st c
 	   | Res_pf_THEN_trivial_fail (term,cl) ->
                tclTHEN (unify_e_resolve st (term,cl)) 
 		 (e_trivial_fail_db true db_list local_db)