Use the proper unification flags in e_exact. This makes exact fail a bit

more often but respects the spec better. The changes in the stdlib are
reduced to adding a few explicit [unfold]s in FMapFacts (exact was doing
conversion with delta on open terms in that case).
Also fix a minor bug in typeclasses not seeing typeclass evars when
their type was a (defined) evar itself.


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

3 files changed, 10 insertions, 11 deletions

diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index 2b9a48030b..b163ed32a2 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -91,7 +91,7 @@ open Auto
 let e_give_exact 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 (* ~flags *) t1) (exact_no_check c) gl
+      tclTHEN (Clenvtac.unify ~flags t1) (exact_no_check c) gl
     else exact_check c gl
 (*   let t1 = (pf_type_of gl c) in *)
 (*     tclTHEN (Clenvtac.unify ~flags t1) (exact_no_check c) gl *)
@@ -286,7 +286,8 @@ let hints_tac hints =
 	    aux (succ i) tl) 
 	  in
 	  let glsv = {it = list_map_i (fun j g -> g, 
-	    { info with auto_depth = j :: i :: info.auto_depth; auto_last_tac = pp }) 1 gls; sigma = s}, fun _ -> v in
+	    { info with auto_depth = j :: i :: info.auto_depth; 
+	      auto_last_tac = pp }) 1 gls; sigma = s}, fun _ -> v in
 	    sk glsv fk
       | [] -> fk ()
     in aux 1 tacs }
@@ -477,8 +478,8 @@ let resolve_typeclass_evars d p env evd onlyargs split fail =
   let pred = 
     if onlyargs then 
       (fun ev evi -> Typeclasses.is_implicit_arg (snd (Evd.evar_source ev evd)) &&
-	Typeclasses.is_class_evar evi)
-    else (fun ev evi -> Typeclasses.is_class_evar evi)
+	Typeclasses.is_class_evar evd evi)
+    else (fun ev evi -> Typeclasses.is_class_evar evd evi)
   in resolve_all_evars d p env pred evd split fail
     
 let solve_inst debug mode depth env evd onlyargs split fail =
diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4
index 09fc808c62..231483dc44 100644
--- a/tactics/eauto.ml4
+++ b/tactics/eauto.ml4
@@ -31,7 +31,7 @@ open Auto
 open Rawterm
 open Hiddentac
 
-let e_give_exact ?(flags=Unification.default_unify_flags) c gl = let t1 = (pf_type_of gl c) and t2 = pf_concl gl in 
+let e_give_exact ?(flags=auto_unif_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 ~flags t1) (exact_check c) gl
   else exact_check c gl
@@ -49,10 +49,8 @@ TACTIC EXTEND eexact
 | [ "eexact" constr(c) ] -> [ e_give_exact c ]
 END
 
-let e_give_exact_constr = h_eexact
-
 let registered_e_assumption gl = 
-  tclFIRST (List.map (fun id gl -> e_give_exact_constr (mkVar id) gl) 
+  tclFIRST (List.map (fun id gl -> e_give_exact (mkVar id) gl) 
               (pf_ids_of_hyps gl)) gl
 
 (************************************************************************)
@@ -137,7 +135,7 @@ and e_my_find_search_nodelta db_list local_db hdc concl =
 	 match t with
 	   | Res_pf (term,cl) -> unify_resolve_nodelta (term,cl)
 	   | ERes_pf (term,cl) -> unify_e_resolve_nodelta (term,cl)
-	   | Give_exact (c) -> e_give_exact_constr c
+	   | Give_exact (c) -> e_give_exact c
 	   | Res_pf_THEN_trivial_fail (term,cl) ->
                tclTHEN (unify_e_resolve_nodelta (term,cl)) 
 		 (e_trivial_fail_db false db_list local_db)
@@ -267,7 +265,7 @@ module SearchProblem = struct
 	let l = 
 	  filter_tactics s.tacres
 	    (List.map 
-	       (fun id -> (e_give_exact_constr (mkVar id),
+	       (fun id -> (e_give_exact (mkVar id),
 			   (str "exact" ++ spc () ++ pr_id id)))
 	       (pf_ids_of_hyps g))
 	in
diff --git a/tactics/eauto.mli b/tactics/eauto.mli
index 1c6f9920fa..d2ac36fe82 100644
--- a/tactics/eauto.mli
+++ b/tactics/eauto.mli
@@ -25,7 +25,7 @@ val e_assumption : tactic
 
 val registered_e_assumption : tactic
 
-val e_give_exact_constr : constr -> tactic
+val e_give_exact : ?flags:Unification.unify_flags -> constr -> tactic
 
 val gen_eauto : bool -> bool * int -> constr list -> 
   hint_db_name list option -> tactic