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

1 files changed, 10 insertions, 5 deletions

diff --git a/contrib/interface/blast.ml b/contrib/interface/blast.ml
index 4df6108b6f..10fafaefc7 100644
--- a/contrib/interface/blast.ml
+++ b/contrib/interface/blast.ml
@@ -168,11 +168,14 @@ let rec e_trivial_fail_db db_list local_db goal =
 
 and e_my_find_search db_list local_db hdc concl = 
   let hdc = head_of_constr_reference hdc in
+  let flags = Auto.auto_unif_flags 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) -> List.map (fun x -> ({flags with Unification.modulo_delta = st}, 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) -> List.map (fun x -> ({flags with Unification.modulo_delta = st}, 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} as _patac)) -> 
@@ -380,12 +383,14 @@ let rec trivial_fail_db db_list local_db gl =
 	(trivial_resolve db_list local_db (pf_concl gl)))) gl
 
 and my_find_search db_list local_db hdc concl =
+  let flags = Auto.auto_unif_flags in
   let tacl = 
     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) -> List.map (fun x -> {flags with Unification.modulo_delta = st}, 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) -> List.map (fun x -> {flags with Unification.modulo_delta = st}, x)
+	(Hint_db.map_auto (hdc,concl) db)) (local_db::db_list)
   in
   List.map 
     (fun (st, {pri=b; pat=p; code=t} as _patac) ->