Backtrack on using metas eagerly in auto, only done in "new auto" for

now. Fix proof scripts that failed correspondingly. Should make many
contribs compile again...


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

3 files changed, 27 insertions, 12 deletions

diff --git a/tactics/auto.ml b/tactics/auto.ml
index 0b1f29dc3b..816bd61ca0 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -591,9 +591,9 @@ let auto_unif_flags = {
 
 (* Try unification with the precompiled clause, then use registered Apply *)
 
-let unify_resolve st (c,clenv) gls = 
+let unify_resolve flags (c,clenv) gls = 
   let clenv' = connect_clenv gls clenv in
-  let _ = clenv_unique_resolver false ~flags:{auto_unif_flags with modulo_delta = st} clenv' gls in  
+  let _ = clenv_unique_resolver false ~flags clenv' gls in  
   h_apply true false (c,NoBindings) gls
 
 (* builds a hint database from a constr signature *)
@@ -649,24 +649,32 @@ let rec trivial_fail_db mod_delta db_list local_db gl =
        (trivial_resolve mod_delta db_list local_db (pf_concl gl)))) gl
 
 and my_find_search mod_delta db_list local_db hdc concl =
+  let flags = 
+    if mod_delta then {auto_unif_flags with use_metas_eagerly = true}
+    else auto_unif_flags
+  in
   let tacl = 
     if occur_existential concl then 
       list_map_append
 	(fun (st, db) -> 
-	  let st = if mod_delta then st else empty_transparent_state in
+	  let st = 
+	    if mod_delta then
+	      {flags with modulo_delta = st} 
+	    else flags 
+	  in
 	    List.map (fun x -> (st,x)) (Hint_db.map_all hdc db))
 	(local_db::db_list)
     else
       list_map_append (fun ((ids, csts as st), db) -> 
 	let st, l = 
 	  if not mod_delta then
-	    empty_transparent_state, Hint_db.map_auto (hdc,concl) db
+	    flags, Hint_db.map_auto (hdc,concl) db
 	  else 
 	    let l =
 	      if (Idpred.is_empty ids && Cpred.is_empty csts)
 	      then Hint_db.map_auto (hdc,concl) db
 	      else Hint_db.map_all hdc db
-	    in st, l
+	    in {flags with modulo_delta = st}, l
 	in List.map (fun x -> (st,x)) l)
       	(local_db::db_list)
   in
diff --git a/tactics/auto.mli b/tactics/auto.mli
index 91f4182fad..7853235be0 100644
--- a/tactics/auto.mli
+++ b/tactics/auto.mli
@@ -138,8 +138,10 @@ val priority : (int * 'a) list -> 'a list
 
 val default_search_depth : int ref
 
+val auto_unif_flags : Unification.unify_flags
+
 (* Try unification with the precompiled clause, then use registered Apply *)
-val unify_resolve : transparent_state -> (constr * clausenv) -> tactic
+val unify_resolve : Unification.unify_flags -> (constr * clausenv) -> tactic
 
 (* [ConclPattern concl pat tacast]:
    if the term concl matches the pattern pat, (in sense of 
diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4
index 62d137b7ae..3894dfd1f7 100644
--- a/tactics/eauto.ml4
+++ b/tactics/eauto.ml4
@@ -85,14 +85,15 @@ TACTIC EXTEND prolog
 END
 
 open Auto
+open Unification
 
 (***************************************************************************)
 (* A tactic similar to Auto, but using EApply, Assumption and e_give_exact *)
 (***************************************************************************)
 
-let unify_e_resolve  (c,clenv) gls = 
+let unify_e_resolve flags (c,clenv) gls = 
   let clenv' = connect_clenv gls clenv in
-  let _ = clenv_unique_resolver false clenv' gls in
+  let _ = clenv_unique_resolver false ~flags clenv' gls in
   h_simplest_eapply c gls
 
 let rec e_trivial_fail_db db_list local_db goal =
@@ -112,9 +113,13 @@ 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 
-      list_map_append (fun (st, db) -> List.map (fun x -> st, x) (Hint_db.map_all hdc db)) (local_db::db_list)
+      list_map_append (fun (st, db) -> 
+	let flags = {auto_unif_flags with modulo_delta = st} in
+	  List.map (fun x -> flags, x) (Hint_db.map_all hdc db)) (local_db::db_list)
     else 
-      list_map_append (fun (st, db) -> List.map (fun x -> st, x) (Hint_db.map_auto (hdc,concl) db)) (local_db::db_list)
+      list_map_append (fun (st, db) -> 
+	let flags = {auto_unif_flags with modulo_delta = st} in
+	  List.map (fun x -> flags, x) (Hint_db.map_auto (hdc,concl) db)) (local_db::db_list)
   in 
   let tac_of_hint = 
     fun (st, {pri=b; pat = p; code=t}) -> 
@@ -122,10 +127,10 @@ and e_my_find_search db_list local_db hdc concl =
        let tac =
 	 match t with
 	   | Res_pf (term,cl) -> unify_resolve st (term,cl)
-	   | ERes_pf (term,cl) -> unify_e_resolve (term,cl)
+	   | ERes_pf (term,cl) -> unify_e_resolve st (term,cl)
 	   | Give_exact (c) -> e_give_exact_constr c
 	   | Res_pf_THEN_trivial_fail (term,cl) ->
-               tclTHEN (unify_e_resolve (term,cl)) 
+               tclTHEN (unify_e_resolve st (term,cl)) 
 		 (e_trivial_fail_db db_list local_db)
 	   | Unfold_nth c -> unfold_in_concl [[],c]
 	   | Extern tacast -> conclPattern concl