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

9 files changed, 49 insertions, 19 deletions

diff --git a/contrib/interface/blast.ml b/contrib/interface/blast.ml
index 4df6108b6..10fafaefc 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) -> 
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 578afdb75..1063342e5 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -145,7 +145,8 @@ let expand_constant env flags c =
 let unify_0_with_initial_metas subst conv_at_top env sigma cv_pb flags m n =
   let nb = nb_rel env in
   let trivial_unify pb (metasubst,_) m n =
-    match subst_defined_metas metasubst m with
+    let subst = if flags.use_metas_eagerly then metasubst else fst subst in
+    match subst_defined_metas subst m with
     | Some m ->
 	(match flags.modulo_conv_on_closed_terms with
 	    Some flags ->
diff --git a/tactics/auto.ml b/tactics/auto.ml
index 0b1f29dc3..816bd61ca 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 91f4182fa..7853235be 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 62d137b7a..3894dfd1f 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 
diff --git a/test-suite/bugs/closed/shouldsucceed/1784.v b/test-suite/bugs/closed/shouldsucceed/1784.v
index d6b7660b2..616dd26f5 100644
--- a/test-suite/bugs/closed/shouldsucceed/1784.v
+++ b/test-suite/bugs/closed/shouldsucceed/1784.v
@@ -85,7 +85,7 @@ Program Fixpoint lt_dec (x y:sv) { struct x } : {slt x y}+{~slt x y} :=
       end
   end.
 
-Next Obligation. apply H; inversion H0; subst; trivial. reflexivity. Defined.
+Next Obligation. apply H; inversion H0; subst; trivial. Defined.
 Next Obligation. inversion H. Defined.
 Next Obligation. inversion H. Defined.
 Next Obligation. inversion H; subst. Defined.
diff --git a/theories/Ints/num/NMake.v b/theories/Ints/num/NMake.v
index c857da385..8cb779350 100644
--- a/theories/Ints/num/NMake.v
+++ b/theories/Ints/num/NMake.v
@@ -5182,6 +5182,7 @@ Qed.
    rewrite H1; simpl Z_of_nat; change (2^1) with (2).
    unfold base.
    apply Zpower_le_monotone; split; auto with zarith.
+   apply Zeq_le; apply Zmult_comm.
  intros n; case n; clear n.
  intros H1; rewrite spec_reduce_2; unfold to_Z.
  apply (znz_of_pos_correct w2_spec).
@@ -5189,6 +5190,7 @@ Qed.
    rewrite H1; simpl Z_of_nat; change (2^2) with (2 * 2).
    unfold base.
    apply Zpower_le_monotone; split; auto with zarith.
+   apply Zeq_le; apply Zmult_comm.
  intros n; case n; clear n.
  intros H1; rewrite spec_reduce_3; unfold to_Z.
  apply (znz_of_pos_correct w3_spec).
@@ -5196,6 +5198,7 @@ Qed.
    rewrite H1; simpl Z_of_nat; change (2^3) with (2 * 2 * 2).
    unfold base.
    apply Zpower_le_monotone; split; auto with zarith. 
+   apply Zeq_le; apply Zmult_comm.
  intros n; case n; clear n.
  intros H1; rewrite spec_reduce_4; unfold to_Z.
  apply (znz_of_pos_correct w4_spec).
@@ -5203,6 +5206,7 @@ Qed.
    rewrite H1; simpl Z_of_nat; change (2^4) with (2 * 2 * 2 * 2).
    unfold base.
    apply Zpower_le_monotone; split; auto with zarith.
+   apply Zeq_le; apply Zmult_comm.
  intros n; case n; clear n.
  intros H1; rewrite spec_reduce_5; unfold to_Z.
  apply (znz_of_pos_correct w5_spec).
@@ -5210,6 +5214,7 @@ Qed.
    rewrite H1; simpl Z_of_nat; change (2^5) with (2 * 2 * 2 * 2 * 2).
    unfold base.
    apply Zpower_le_monotone; split; auto with zarith.
+   apply Zeq_le; apply Zmult_comm.
  intros n; case n; clear n.
  intros H1; rewrite spec_reduce_6; unfold to_Z.
  apply (znz_of_pos_correct w6_spec).
@@ -5217,6 +5222,7 @@ Qed.
    rewrite H1; simpl Z_of_nat; change (2^6) with (2 * 2 * 2 * 2 * 2 * 2).
    unfold base.
    apply Zpower_le_monotone; split; auto with zarith.
+   apply Zeq_le; apply Zmult_comm.
  intros n.
  intros H1; rewrite spec_reduce_n; unfold to_Z.
  simpl minus; rewrite <- minus_n_O.
diff --git a/theories/Lists/List.v b/theories/Lists/List.v
index 78a2db534..51d3f192d 100644
--- a/theories/Lists/List.v
+++ b/theories/Lists/List.v
@@ -687,6 +687,7 @@ Section ListOps.
     rewrite (minus_plus_simpl_l_reverse (length l) n 1).
     replace (1 + length l) with (S (length l)); auto with arith.
     rewrite <- minus_Sn_m; auto with arith.
+    apply IHl ; auto with arith.
     rewrite rev_length; auto.
   Qed.
 
@@ -1362,6 +1363,7 @@ End Fold_Right_Recursor.
       destruct n; destruct d; simpl; auto.
       destruct a; destruct (split l); simpl; auto.
       destruct a; destruct (split l); simpl in *; auto.
+      apply IHl.
     Qed.
 
     Lemma split_length_l : forall (l:list (A*B)),
diff --git a/theories/ZArith/Zpow_facts.v b/theories/ZArith/Zpow_facts.v
index 9524bd44f..8f86fdf79 100644
--- a/theories/ZArith/Zpow_facts.v
+++ b/theories/ZArith/Zpow_facts.v
@@ -171,6 +171,7 @@ Qed.
 Theorem Zpower_ge_0: forall x y, 0 <= x -> 0 <= x^y. 
 Proof.
   intros x y; case y; auto with zarith.
+  simpl ; auto with zarith.
   intros p H1; assert (H: 0 <= Zpos p); auto with zarith.
   generalize H; pattern (Zpos p); apply natlike_ind; auto with zarith.
   intros p1 H2 H3 _; unfold Zsucc; rewrite Zpower_exp; simpl; auto with zarith.