Fix bug #1704 (ordering of condition goals for (setoid)rewrite). As part

of the fix I added an optional "by" annotation for rewrite to solve said
conditions in the same tactic call. Most of the theories have been
updated, only FSets is missing, Pierre will take care of it.


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

3 files changed, 12 insertions, 12 deletions

diff --git a/theories/Numbers/Natural/Abstract/NIso.v b/theories/Numbers/Natural/Abstract/NIso.v
index 10c341cbfa..4df46e20eb 100644
--- a/theories/Numbers/Natural/Abstract/NIso.v
+++ b/theories/Numbers/Natural/Abstract/NIso.v
@@ -51,8 +51,8 @@ Theorem natural_isomorphism_succ :
   forall n : N1, natural_isomorphism (S1 n) == S2 (natural_isomorphism n).
 Proof.
 unfold natural_isomorphism.
-intro n. now rewrite (@NAxiomsMod1.recursion_succ N2 NAxiomsMod2.Neq);
-[| unfold fun2_wd; intros; apply NBasePropMod2.succ_wd |].
+intro n. now rewrite (@NAxiomsMod1.recursion_succ N2 NAxiomsMod2.Neq) ;
+[ | | unfold fun2_wd; intros; apply NBasePropMod2.succ_wd].
 Qed.
 
 Theorem hom_nat_iso : homomorphism natural_isomorphism.
diff --git a/theories/Numbers/Natural/Abstract/NMinus.v b/theories/Numbers/Natural/Abstract/NMinus.v
index faf4759bdb..5e1d5d8c3c 100644
--- a/theories/Numbers/Natural/Abstract/NMinus.v
+++ b/theories/Numbers/Natural/Abstract/NMinus.v
@@ -63,8 +63,8 @@ Proof.
 intros n m p; induct p.
 intro; now do 2 rewrite minus_0_r.
 intros p IH H. do 2 rewrite minus_succ_r.
-rewrite <- IH; [apply lt_le_incl; now apply -> le_succ_l |].
-rewrite plus_pred_r. apply minus_gt. now apply -> le_succ_l.
+rewrite <- IH by (apply lt_le_incl; now apply -> le_succ_l).
+rewrite plus_pred_r by (apply minus_gt; now apply -> le_succ_l).
 reflexivity.
 Qed.
 
@@ -76,13 +76,13 @@ Qed.
 
 Theorem plus_minus : forall n m : N, (n + m) - m == n.
 Proof.
-intros n m. rewrite <- plus_minus_assoc. apply le_refl.
+intros n m. rewrite <- plus_minus_assoc by (apply le_refl).
 rewrite minus_diag; now rewrite plus_0_r.
 Qed.
 
 Theorem minus_plus : forall n m : N, n <= m -> (m - n) + n == m.
 Proof.
-intros n m H. rewrite plus_comm. rewrite plus_minus_assoc; [assumption |].
+intros n m H. rewrite plus_comm. rewrite plus_minus_assoc by assumption.
 rewrite plus_comm. apply plus_minus.
 Qed.
 
@@ -121,7 +121,7 @@ Theorem plus_minus_swap : forall n m p : N, p <= n -> n + m - p == n - p + m.
 Proof.
 intros n m p H.
 rewrite (plus_comm n m).
-rewrite <- plus_minus_assoc; [assumption |].
+rewrite <- plus_minus_assoc by assumption.
 now rewrite (plus_comm m (n - p)).
 Qed.
 
@@ -151,8 +151,8 @@ Proof.
 intros n m; cases m.
 now rewrite pred_0, times_0_r, minus_0_l.
 intro m; rewrite pred_succ, times_succ_r, <- plus_minus_assoc.
-now apply eq_le_incl.
 now rewrite minus_diag, plus_0_r.
+now apply eq_le_incl.
 Qed.
 
 Theorem times_minus_distr_r : forall n m p : N, (n - m) * p == n * p - m * p.
@@ -160,9 +160,9 @@ Proof.
 intros n m p; induct n.
 now rewrite minus_0_l, times_0_l, minus_0_l.
 intros n IH. destruct (le_gt_cases m n) as [H | H].
-rewrite minus_succ_l; [assumption |]. do 2 rewrite times_succ_l.
+rewrite minus_succ_l by assumption. do 2 rewrite times_succ_l.
 rewrite (plus_comm ((n - m) * p) p), (plus_comm (n * p) p).
-rewrite <- (plus_minus_assoc p (n * p) (m * p)); [now apply times_le_mono_r |].
+rewrite <- (plus_minus_assoc p (n * p) (m * p)) by now apply times_le_mono_r.
 now apply <- plus_cancel_l.
 assert (H1 : S n <= m); [now apply <- le_succ_l |].
 setoid_replace (S n - m) with 0 by now apply <- minus_0_le.
diff --git a/theories/Numbers/Natural/Abstract/NOrder.v b/theories/Numbers/Natural/Abstract/NOrder.v
index 7b4645be35..1e53d80637 100644
--- a/theories/Numbers/Natural/Abstract/NOrder.v
+++ b/theories/Numbers/Natural/Abstract/NOrder.v
@@ -506,7 +506,7 @@ Theorem pred_lt_mono : forall n m : N, n ~= 0 -> (n < m <-> P n < P m).
 Proof.
 intros n m H1; split; intro H2.
 assert (m ~= 0). apply <- neq_0_lt_0. now apply lt_lt_0 with n.
-now rewrite <- (succ_pred n) in H2; rewrite <- (succ_pred m) in H2;
+now rewrite <- (succ_pred n) in H2; rewrite <- (succ_pred m) in H2 ;
 [apply <- succ_lt_mono | | |].
 assert (m ~= 0). apply <- neq_0_lt_0. apply lt_lt_0 with (P n).
 apply lt_le_trans with (P m). assumption. apply le_pred_l.
@@ -515,7 +515,7 @@ Qed.
 
 Theorem lt_succ_lt_pred : forall n m : N, S n < m <-> n < P m.
 Proof.
-intros n m. rewrite pred_lt_mono. apply neq_succ_0. now rewrite pred_succ.
+intros n m. rewrite pred_lt_mono by apply neq_succ_0. now rewrite pred_succ.
 Qed.
 
 Theorem le_succ_le_pred : forall n m : N, S n <= m -> n <= P m. (* Converse is false for n == m == 0 *)