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

2 files changed, 11 insertions, 11 deletions

diff --git a/theories/Numbers/NatInt/NZOrder.v b/theories/Numbers/NatInt/NZOrder.v
index bc3600f9ce..133bbde4df 100644
--- a/theories/Numbers/NatInt/NZOrder.v
+++ b/theories/Numbers/NatInt/NZOrder.v
@@ -140,11 +140,12 @@ setoid_replace (n < n) with False using relation iff by
 now setoid_replace (S n <= n) with False using relation iff by
   (apply -> neg_false; apply NZnle_succ_diag_l).
 intro m. rewrite NZlt_succ_r. rewrite NZle_succ_r.
-rewrite NZsucc_inj_wd. rewrite (NZlt_eq_cases n m).
+rewrite NZsucc_inj_wd.
+rewrite (NZlt_eq_cases n m).
 rewrite or_cancel_r.
+reflexivity.
 intros H1 H2; rewrite H2 in H1; false_hyp H1 NZnle_succ_diag_l.
 apply NZlt_neq.
-reflexivity.
 Qed.
 
 Theorem NZlt_succ_l : forall n m : NZ, S n < m -> n < m.
diff --git a/theories/Numbers/NatInt/NZTimesOrder.v b/theories/Numbers/NatInt/NZTimesOrder.v
index 51d2172dec..b51e3d22b6 100644
--- a/theories/Numbers/NatInt/NZTimesOrder.v
+++ b/theories/Numbers/NatInt/NZTimesOrder.v
@@ -60,7 +60,7 @@ split; [apply LR |]. intro H2. apply -> NZlt_dne; intro H3.
 apply <- NZle_ngt in H3. le_elim H3.
 apply NZlt_asymm in H2. apply H2. now apply LR.
 rewrite H3 in H2; false_hyp H2 NZlt_irrefl.
-rewrite (NZtimes_lt_pred p (S p)); [reflexivity |].
+rewrite (NZtimes_lt_pred p (S p)) by reflexivity.
 rewrite H; do 2 rewrite NZtimes_0_l; now do 2 rewrite NZplus_0_l.
 Qed.
 
@@ -109,9 +109,9 @@ assert (H4 : p * n < p * m); [now apply -> NZtimes_lt_mono_neg_l |].
 rewrite H1 in H4; false_hyp H4 NZlt_irrefl.
 false_hyp H2 H.
 apply -> NZeq_dne; intro H3. apply -> NZlt_gt_cases in H3. destruct H3 as [H3 | H3].
-assert (H4 : p * n < p * m); [now apply -> NZtimes_lt_mono_pos_l |].
+assert (H4 : p * n < p * m) by (now apply -> NZtimes_lt_mono_pos_l).
 rewrite H1 in H4; false_hyp H4 NZlt_irrefl.
-assert (H4 : p * m < p * n); [now apply -> NZtimes_lt_mono_pos_l |].
+assert (H4 : p * m < p * n) by (now apply -> NZtimes_lt_mono_pos_l).
 rewrite H1 in H4; false_hyp H4 NZlt_irrefl.
 now rewrite H1.
 Qed.
@@ -135,9 +135,9 @@ Qed.
 Theorem NZtimes_le_mono_pos_l : forall n m p : NZ, 0 < p -> (n <= m <-> p * n <= p * m).
 Proof.
 intros n m p H; do 2 rewrite NZlt_eq_cases.
-rewrite (NZtimes_lt_mono_pos_l p n m); [assumption |].
-now rewrite -> (NZtimes_cancel_l n m p);
-[intro H1; rewrite H1 in H; false_hyp H NZlt_irrefl |].
+rewrite (NZtimes_lt_mono_pos_l p n m) by assumption.
+now rewrite -> (NZtimes_cancel_l n m p) by
+(intro H1; rewrite H1 in H; false_hyp H NZlt_irrefl).
 Qed.
 
 Theorem NZtimes_le_mono_pos_r : forall n m p : NZ, 0 < p -> (n <= m <-> n * p <= m * p).
@@ -149,9 +149,8 @@ Qed.
 Theorem NZtimes_le_mono_neg_l : forall n m p : NZ, p < 0 -> (n <= m <-> p * m <= p * n).
 Proof.
 intros n m p H; do 2 rewrite NZlt_eq_cases.
-rewrite (NZtimes_lt_mono_neg_l p n m); [assumption |].
-rewrite -> (NZtimes_cancel_l m n p);
-[intro H1; rewrite H1 in H; false_hyp H NZlt_irrefl |].
+rewrite (NZtimes_lt_mono_neg_l p n m); [| assumption].
+rewrite -> (NZtimes_cancel_l m n p) by (intro H1; rewrite H1 in H; false_hyp H NZlt_irrefl).
 now setoid_replace (n == m) with (m == n) using relation iff by (split; now intro).
 Qed.