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, 9 insertions, 0 deletions

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.