Simplify eauto and fix it for compatibility, allowing full delta during

unification for exact hints.


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

2 files changed, 15 insertions, 58 deletions

diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4
index 231483dc44..3a16cd7935 100644
--- a/tactics/eauto.ml4
+++ b/tactics/eauto.ml4
@@ -31,7 +31,9 @@ open Auto
 open Rawterm
 open Hiddentac
 
-let e_give_exact ?(flags=auto_unif_flags) c gl = let t1 = (pf_type_of gl c) and t2 = pf_concl gl in 
+let eauto_unif_flags = { auto_unif_flags with Unification.modulo_delta = full_transparent_state }
+
+let e_give_exact ?(flags=eauto_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
@@ -91,70 +93,25 @@ open Unification
 
 let priority l = List.map snd (List.filter (fun (pr,_) -> pr = 0) l)
 
-(* no delta yet *)
-
 let unify_e_resolve flags (c,clenv) gls = 
   let clenv' = connect_clenv gls clenv in
   let _ = clenv_unique_resolver false ~flags clenv' gls in
   h_simplest_eapply c gls
 
-let unify_e_resolve_nodelta (c,clenv) gls = 
-  let clenv' = connect_clenv gls clenv in
-  let _ = clenv_unique_resolver false clenv' gls in
-  h_simplest_eapply c gls
-
-let rec e_trivial_fail_db mod_delta db_list local_db goal =
+let rec e_trivial_fail_db db_list local_db goal =
   let tacl = 
     registered_e_assumption ::
     (tclTHEN Tactics.intro 
        (function g'->
 	  let d = pf_last_hyp g' in
 	  let hintl = make_resolve_hyp (pf_env g') (project g') d in
-          (e_trivial_fail_db mod_delta db_list
+          (e_trivial_fail_db db_list
 	      (Hint_db.add_list hintl local_db) g'))) ::
-    (List.map fst (e_trivial_resolve mod_delta db_list local_db (pf_concl goal)) )
+    (List.map fst (e_trivial_resolve db_list local_db (pf_concl goal)) )
   in 
   tclFIRST (List.map tclCOMPLETE tacl) goal 
 
-and e_my_find_search mod_delta =
-  if mod_delta then e_my_find_search_delta
-  else e_my_find_search_nodelta
-
-and e_my_find_search_nodelta db_list local_db hdc concl = 
-  let hdc = head_of_constr_reference hdc in
-  let hintl =
-    if occur_existential concl then 
-      list_map_append (Hint_db.map_all hdc) (local_db::db_list)
-    else 
-      list_map_append (Hint_db.map_auto (hdc,concl)) (local_db::db_list)
-  in 
-  let tac_of_hint = 
-    fun {pri=b; pat = p; code=t} -> 
-      (b, 
-       let tac =
-	 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 c
-	   | Res_pf_THEN_trivial_fail (term,cl) ->
-               tclTHEN (unify_e_resolve_nodelta (term,cl)) 
-		 (e_trivial_fail_db false db_list local_db)
-	   | Unfold_nth c -> unfold_in_concl [all_occurrences,c]
-	   | Extern tacast -> conclPattern concl p tacast
-       in 
-       (tac,pr_autotactic t))
-       (*i
-	 fun gls -> pPNL (pr_autotactic t); Format.print_flush (); 
-                     try tac gls
-		     with e when Logic.catchable_exception(e) -> 
-                            (Format.print_string "Fail\n"; 
-			     Format.print_flush (); 
-			     raise e)
-       i*)
-  in 
-  List.map tac_of_hint hintl
-
-and e_my_find_search_delta db_list local_db hdc concl = 
+and e_my_find_search db_list local_db hdc concl = 
   let hdc = head_of_constr_reference hdc in
   let hintl =
     if occur_existential concl then 
@@ -173,10 +130,10 @@ 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 ~flags:st c
+	   | Give_exact (c) -> e_give_exact c
 	   | Res_pf_THEN_trivial_fail (term,cl) ->
                tclTHEN (unify_e_resolve st (term,cl)) 
-		 (e_trivial_fail_db true db_list local_db)
+		 (e_trivial_fail_db db_list local_db)
 	   | Unfold_nth c -> unfold_in_concl [all_occurrences,c]
 	   | Extern tacast -> conclPattern concl p tacast
        in 
@@ -192,16 +149,16 @@ and e_my_find_search_delta db_list local_db hdc concl =
   in 
   List.map tac_of_hint hintl
     
-and e_trivial_resolve mod_delta db_list local_db gl = 
+and e_trivial_resolve db_list local_db gl = 
   try 
     priority 
-      (e_my_find_search mod_delta db_list local_db 
+      (e_my_find_search db_list local_db 
 	 (fst (head_constr_bound gl)) gl)
   with Bound | Not_found -> []
 
-let e_possible_resolve mod_delta db_list local_db gl =
+let e_possible_resolve db_list local_db gl =
   try List.map snd 
-    (e_my_find_search mod_delta db_list local_db 
+    (e_my_find_search db_list local_db 
 	(fst (head_constr_bound gl)) gl)
   with Bound | Not_found -> []
 
@@ -288,7 +245,7 @@ module SearchProblem = struct
       in
       let rec_tacs = 
 	let l = 
-	  filter_tactics s.tacres (e_possible_resolve false s.dblist (List.hd s.localdb) (pf_concl g))
+	  filter_tactics s.tacres (e_possible_resolve s.dblist (List.hd s.localdb) (pf_concl g))
 	in
 	List.map 
 	  (fun ((lgls,_) as res, pp) -> 
diff --git a/theories/FSets/FMapFacts.v b/theories/FSets/FMapFacts.v
index cd80003a26..e116067afd 100644
--- a/theories/FSets/FMapFacts.v
+++ b/theories/FSets/FMapFacts.v
@@ -790,7 +790,7 @@ Module WProperties_fun (E:DecidableType)(M:WSfun E).
   intros. symmetry.
   unfold eqb.
   rewrite <- findA_NoDupA, InA_rev, findA_NoDupA
-   by eauto using NoDupA_rev; eauto. apply H0.
+   by eauto using NoDupA_rev; eauto.
   case_eq (findA (eqb k) (rev l)); auto.
   intros e.
   unfold eqb.