"by" becomes officially a reserved keyword of Coq (fixes "rewrite ... at ... by ...")

 Application in some proofs of Numbers's abstract division

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

4 files changed, 22 insertions, 22 deletions

diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index ef41f938d..c845daf2c 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -22,7 +22,7 @@ open Termops
 
 let all_with delta = make_red_flag [FBeta;FIota;FZeta;delta]
 
-let tactic_kw = [ "->"; "<-" ]
+let tactic_kw = [ "->"; "<-" ; "by" ]
 let _ = List.iter (fun s -> Lexer.add_token("",s)) tactic_kw
 
 (* Hack to parse "(x:=t)" as an explicit argument without conflicts with the *)
@@ -478,11 +478,11 @@ GEXTEND Gram
     [ [ "as"; id = ident -> Names.Name id | -> Names.Anonymous ] ]
   ;
   by_tactic:
-    [ [ IDENT "by"; tac = tactic_expr LEVEL "3" -> TacComplete tac
+    [ [ "by"; tac = tactic_expr LEVEL "3" -> TacComplete tac
       | -> TacId [] ] ]
   ;
   opt_by_tactic:
-    [ [ IDENT "by"; tac = tactic_expr LEVEL "3" -> Some tac
+    [ [ "by"; tac = tactic_expr LEVEL "3" -> Some tac
     | -> None ] ]
   ;
   rename :
diff --git a/theories/Numbers/Integer/Abstract/ZDivEucl.v b/theories/Numbers/Integer/Abstract/ZDivEucl.v
index a853395a6..914055654 100644
--- a/theories/Numbers/Integer/Abstract/ZDivEucl.v
+++ b/theories/Numbers/Integer/Abstract/ZDivEucl.v
@@ -385,7 +385,7 @@ nzsimpl.
 rewrite (add_lt_mono_r _ _ (a mod c)).
 rewrite <- div_mod by order.
 apply lt_le_trans with b; trivial.
-rewrite (div_mod b c) at 1; [| order].
+rewrite (div_mod b c) at 1 by order.
 rewrite <- add_assoc, <- add_le_mono_l.
 apply le_trans with (c+0).
 nzsimpl; destruct (mod_always_pos b c); try order.
@@ -524,7 +524,7 @@ rewrite abs_mul, (abs_pos c) by order.
 rewrite <-(mul_0_l c), <-mul_lt_mono_pos_r, <-mul_le_mono_pos_r by trivial.
 apply mod_always_pos.
 (* equation *)
-rewrite (div_mod a b) at 1; [|order].
+rewrite (div_mod a b) at 1 by order.
 rewrite mul_add_distr_r.
 rewrite add_cancel_r.
 rewrite <- 2 mul_assoc. now rewrite (mul_comm c).
@@ -568,7 +568,7 @@ Lemma mul_mod_idemp_l : forall a b n, n~=0 ->
  ((a mod n)*b) mod n == (a*b) mod n.
 Proof.
  intros a b n Hn. symmetry.
- rewrite (div_mod a n) at 1; [|order].
+ rewrite (div_mod a n) at 1 by order.
  rewrite add_comm, (mul_comm n), (mul_comm _ b).
  rewrite mul_add_distr_l, mul_assoc.
  rewrite mod_add by trivial.
@@ -591,7 +591,7 @@ Lemma add_mod_idemp_l : forall a b n, n~=0 ->
  ((a mod n)+b) mod n == (a+b) mod n.
 Proof.
  intros a b n Hn. symmetry.
- rewrite (div_mod a n) at 1; [|order].
+ rewrite (div_mod a n) at 1 by order.
  rewrite <- add_assoc, add_comm, mul_comm.
  now rewrite mod_add.
 Qed.
@@ -628,7 +628,7 @@ Proof.
  rewrite (abs_pos b) by order.
  now rewrite <- mul_succ_r, <- mul_le_mono_pos_l, le_succ_l.
  (* end 0<= ... < abs(b*c) *)
- rewrite (div_mod a b) at 1; [|order].
+ rewrite (div_mod a b) at 1 by order.
  rewrite add_assoc, add_cancel_r.
  rewrite <- mul_assoc, <- mul_add_distr_l, mul_cancel_l by order.
  apply div_mod; order.
diff --git a/theories/Numbers/Integer/Abstract/ZDivFloor.v b/theories/Numbers/Integer/Abstract/ZDivFloor.v
index 551ce6b41..611432a6d 100644
--- a/theories/Numbers/Integer/Abstract/ZDivFloor.v
+++ b/theories/Numbers/Integer/Abstract/ZDivFloor.v
@@ -354,7 +354,7 @@ nzsimpl.
 rewrite (add_lt_mono_r _ _ (a mod c)).
 rewrite <- div_mod by order.
 apply lt_le_trans with b; trivial.
-rewrite (div_mod b c) at 1; [| order].
+rewrite (div_mod b c) at 1 by order.
 rewrite <- add_assoc, <- add_le_mono_l.
 apply le_trans with (c+0).
 nzsimpl; destruct (mod_pos_bound b c); order.
@@ -495,7 +495,7 @@ now apply mod_bound_or.
 rewrite <-(mul_0_l c), <-2mul_lt_mono_neg_r, <-2mul_le_mono_neg_r by order.
 destruct (mod_bound_or a b); tauto.
 (* equation *)
-rewrite (div_mod a b) at 1; [|order].
+rewrite (div_mod a b) at 1 by order.
 rewrite mul_add_distr_r.
 rewrite add_cancel_r.
 rewrite <- 2 mul_assoc. now rewrite (mul_comm c).
@@ -539,7 +539,7 @@ Lemma mul_mod_idemp_l : forall a b n, n~=0 ->
  ((a mod n)*b) mod n == (a*b) mod n.
 Proof.
  intros a b n Hn. symmetry.
- rewrite (div_mod a n) at 1; [|order].
+ rewrite (div_mod a n) at 1 by order.
  rewrite add_comm, (mul_comm n), (mul_comm _ b).
  rewrite mul_add_distr_l, mul_assoc.
  intros. rewrite mod_add by trivial.
@@ -562,7 +562,7 @@ Lemma add_mod_idemp_l : forall a b n, n~=0 ->
  ((a mod n)+b) mod n == (a+b) mod n.
 Proof.
  intros a b n Hn. symmetry.
- rewrite (div_mod a n) at 1; [|order].
+ rewrite (div_mod a n) at 1 by order.
  rewrite <- add_assoc, add_comm, mul_comm.
  intros. now rewrite mod_add.
 Qed.
@@ -598,7 +598,7 @@ Proof.
  now rewrite <- add_lt_mono_l.
  now rewrite <- mul_succ_r, <- mul_le_mono_pos_l, le_succ_l.
  (* end 0<= ... < b*c \/ ... *)
- rewrite (div_mod a b) at 1; [|order].
+ rewrite (div_mod a b) at 1 by order.
  rewrite add_assoc, add_cancel_r.
  rewrite <- mul_assoc, <- mul_add_distr_l, mul_cancel_l by order.
  apply div_mod; order.
diff --git a/theories/Numbers/NatInt/NZDiv.v b/theories/Numbers/NatInt/NZDiv.v
index db64a7963..da7d62ceb 100644
--- a/theories/Numbers/NatInt/NZDiv.v
+++ b/theories/Numbers/NatInt/NZDiv.v
@@ -247,7 +247,7 @@ intros.
 assert (0 < b) by (apply lt_trans with 1; auto using lt_0_1).
 destruct (lt_ge_cases a b).
 rewrite div_small; try split; order.
-rewrite (div_mod a b) at 2; [|order].
+rewrite (div_mod a b) at 2 by order.
 apply lt_le_trans with (b*(a/b)).
 rewrite <- (mul_1_l (a/b)) at 1.
 rewrite <- mul_lt_mono_pos_r; auto.
@@ -269,7 +269,7 @@ nzsimpl.
 rewrite (add_lt_mono_r _ _ (a mod c)).
 rewrite <- div_mod by order.
 apply lt_le_trans with b; auto.
-rewrite (div_mod b c) at 1; [| order].
+rewrite (div_mod b c) at 1 by order.
 rewrite <- add_assoc, <- add_le_mono_l.
 apply le_trans with (c+0).
 nzsimpl; destruct (mod_bound b c); order.
@@ -289,7 +289,7 @@ Qed.
 Lemma mul_succ_div_gt : forall a b, 0<=a -> 0<b -> a < b*(S (a/b)).
 Proof.
 intros.
-rewrite (div_mod a b) at 1; [|order].
+rewrite (div_mod a b) at 1 by order.
 rewrite (mul_succ_r).
 rewrite <- add_lt_mono_l.
 destruct (mod_bound a b); auto.
@@ -300,7 +300,7 @@ Qed.
 
 Lemma div_exact : forall a b, 0<=a -> 0<b -> (a == b*(a/b) <-> a mod b == 0).
 Proof.
-intros. rewrite (div_mod a b) at 1; [|order].
+intros. rewrite (div_mod a b) at 1 by order.
 rewrite <- (add_0_r (b*(a/b))) at 2.
 apply add_cancel_l.
 Qed.
@@ -344,7 +344,7 @@ Lemma div_le_compat_l: forall p q r, 0<=p -> 0<q<=r ->
 Proof.
  intros p q r Hp (Hq,Hqr).
  apply div_le_lower_bound; auto.
- rewrite (div_mod p r) at 2; [|order].
+ rewrite (div_mod p r) at 2 by order.
  apply le_trans with (r*(p/r)).
  apply mul_le_mono_nonneg_r; try order.
  apply div_pos; order.
@@ -396,7 +396,7 @@ Proof.
  split.
  apply mul_nonneg_nonneg; destruct (mod_bound a b); order.
  rewrite <- mul_lt_mono_pos_r; auto. destruct (mod_bound a b); auto.
- rewrite (div_mod a b) at 1; [|order].
+ rewrite (div_mod a b) at 1 by order.
  rewrite mul_add_distr_r.
  rewrite add_cancel_r.
  rewrite <- 2 mul_assoc. now rewrite (mul_comm c).
@@ -439,7 +439,7 @@ Lemma mul_mod_idemp_l : forall a b n, 0<=a -> 0<=b -> 0<n ->
 Proof.
  intros a b n Ha Hb Hn. symmetry.
  generalize (mul_nonneg_nonneg _ _ Ha Hb).
- rewrite (div_mod a n) at 1 2; [|order].
+ rewrite (div_mod a n) at 1 2 by order.
  rewrite add_comm, (mul_comm n), (mul_comm _ b).
  rewrite mul_add_distr_l, mul_assoc.
  intros. rewrite mod_add; auto.
@@ -465,7 +465,7 @@ Lemma add_mod_idemp_l : forall a b n, 0<=a -> 0<=b -> 0<n ->
 Proof.
  intros a b n Ha Hb Hn. symmetry.
  generalize (add_nonneg_nonneg _ _ Ha Hb).
- rewrite (div_mod a n) at 1 2; [|order].
+ rewrite (div_mod a n) at 1 2 by order.
  rewrite <- add_assoc, add_comm, mul_comm.
  intros. rewrite mod_add; trivial. reflexivity.
  apply add_nonneg_nonneg; auto. destruct (mod_bound a n); auto.
@@ -498,7 +498,7 @@ Proof.
  rewrite <- add_lt_mono_l; auto.
  rewrite <- mul_succ_r, <- mul_le_mono_pos_l, le_succ_l; auto.
  (* end 0<= ... < b*c *)
- rewrite (div_mod a b) at 1; [|order].
+ rewrite (div_mod a b) at 1 by order.
  rewrite add_assoc, add_cancel_r.
  rewrite <- mul_assoc, <- mul_add_distr_l, mul_cancel_l by order.
  apply div_mod; order.