Less ambitious application of a notation for eq_rect. We proposed

"rewrite Heq in H" but "rewrite" is sometimes used by users and I
don't want to have to change their file.

The solution to put the notations in a module does not work with name
"rewrite" because loading the module would change the status of
"rewrite" from simple ident to keyword (and we cannot declare
"rewrite" as an ident, as shown in previous commit).

Then we come back on notation "rew" (this name is also used by some
users), in a module.

This continues commit r14366 and r14390 and improves on the level of
the notation.

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

4 files changed, 19 insertions, 13 deletions

diff --git a/CHANGES b/CHANGES
index 921c9284b6..05ad1d7e01 100644
--- a/CHANGES
+++ b/CHANGES
@@ -89,7 +89,8 @@ Libraries
   Vcons become Vector.cons. You can use notations by importing
   Vector.VectorNotations.
 - Removal of TheoryList. Requiring List instead should work most of the time.
-- New syntax "rew Heq in H" and "rew <- Heq in H" for eq_rect and eq_rect_r.
+- New syntax "rew Heq in H" and "rew <- Heq in H" for eq_rect and 
+  eq_rect_r (available by importing module EqNotations).
 
 Internal infrastructure
 
diff --git a/theories/Init/Logic.v b/theories/Init/Logic.v
index 00a93efa0c..fe3f947da0 100644
--- a/theories/Init/Logic.v
+++ b/theories/Init/Logic.v
@@ -334,12 +334,14 @@ Section Logic_lemmas.
   Defined.
 End Logic_lemmas.
 
-Notation "'rewrite' H 'in' H'" := (eq_rect _ _ H' _ H)
-  (at level 10, H' at level 9).
-Notation "'rewrite' <- H 'in' H'" := (eq_rect_r _ H' H)
-  (at level 10, H' at level 9).
-Notation "'rewrite' -> H 'in' H'" := (eq_rect _ _ H' _ H)
-  (at level 10, H' at level 9, only parsing).
+Module EqNotations.
+  Notation "'rew' H 'in' H'" := (eq_rect _ _ H' _ H)
+    (at level 10, H' at level 10).
+  Notation "'rew' <- H 'in' H'" := (eq_rect_r _ H' H)
+    (at level 10, H' at level 10).
+  Notation "'rew' -> H 'in' H'" := (eq_rect _ _ H' _ H)
+    (at level 10, H' at level 10, only parsing).
+End EqNotations.
 
 Theorem f_equal2 :
   forall (A1 A2 B:Type) (f:A1 -> A2 -> B) (x1 y1:A1)
diff --git a/theories/Logic/EqdepFacts.v b/theories/Logic/EqdepFacts.v
index 8fbd79fa49..a341a7a5a9 100644
--- a/theories/Logic/EqdepFacts.v
+++ b/theories/Logic/EqdepFacts.v
@@ -50,6 +50,8 @@ Table of contents:
 (************************************************************************)
 (** * Definition of dependent equality and equivalence with equality of dependent pairs *)
 
+Import EqNotations.
+
 Section Dependent_Equality.
 
   Variable U : Type.
@@ -84,7 +86,7 @@ Section Dependent_Equality.
       equalities *)
 
   Inductive eq_dep1 (p:U) (x:P p) (q:U) (y:P q) : Prop :=
-    eq_dep1_intro : forall h:q = p, x = rewrite h in y -> eq_dep1 p x q y.
+    eq_dep1_intro : forall h:q = p, x = rew h in y -> eq_dep1 p x q y.
 
   Lemma eq_dep1_dep :
     forall (p:U) (x:P p) (q:U) (y:P q), eq_dep1 p x q y -> eq_dep p x q y.
@@ -164,7 +166,7 @@ Qed.
 
 Set Implicit Arguments.
 
-Lemma eq_sigT_sig_eq : forall X P (x1 x2:X) H1 H2, existT P x1 H1 = existT P x2 H2 <-> {H:x1=x2 | rewrite H in H1 = H2}.
+Lemma eq_sigT_sig_eq : forall X P (x1 x2:X) H1 H2, existT P x1 H1 = existT P x2 H2 <-> {H:x1=x2 | rew H in H1 = H2}.
 Proof.
   intros; split; intro H.
   - change x2 with (projT1 (existT P x2 H2)).
@@ -186,7 +188,7 @@ Proof.
 Defined.
 
 Lemma eq_sigT_snd :
-  forall X P (x1 x2:X) H1 H2 (H:existT P x1 H1 = existT P x2 H2), rewrite (eq_sigT_fst H) in H1 = H2.
+  forall X P (x1 x2:X) H1 H2 (H:existT P x1 H1 = existT P x2 H2), rew (eq_sigT_fst H) in H1 = H2.
 Proof.
   intros.
   unfold eq_sigT_fst.
@@ -206,7 +208,7 @@ Proof.
 Defined.
 
 Lemma eq_sig_snd :
-  forall X P (x1 x2:X) H1 H2 (H:exist P x1 H1 = exist P x2 H2), rewrite (eq_sig_fst H) in H1 = H2.
+  forall X P (x1 x2:X) H1 H2 (H:exist P x1 H1 = exist P x2 H2), rew (eq_sig_fst H) in H1 = H2.
 Proof.
   intros.
   unfold eq_sig_fst, eq_ind.
diff --git a/theories/Vectors/VectorDef.v b/theories/Vectors/VectorDef.v
index 9129b94de1..ad241462eb 100644
--- a/theories/Vectors/VectorDef.v
+++ b/theories/Vectors/VectorDef.v
@@ -18,6 +18,7 @@ have to be the same. complain if you see mistakes ... *)
 
 Require Import Arith_base.
 Require Vectors.Fin.
+Import EqNotations.
 Open Local Scope nat_scope.
 
 (**
@@ -202,13 +203,13 @@ Import EqdepFacts.
 (** This one has a better type *)
 Definition rev_append {A n p} (v: t A n) (w: t A p)
   :t A (n + p) :=
-  rewrite <- (plus_tail_plus n p) in (rev_append_tail v w).
+  rew <- (plus_tail_plus n p) in (rev_append_tail v w).
 
 (** rev [a₁ ; a₂ ; .. ; an] is [an ; a{n-1} ; .. ; a₁]
 
 Caution : There is a lot of rewrite garbage in this definition *)
 Definition rev {A n} (v : t A n) : t A n :=
- rewrite <- (plus_n_O _) in (rev_append v []).
+ rew <- (plus_n_O _) in (rev_append v []).
 
 End BASES.
 Local Notation "v [@ p ]" := (nth v p) (at level 1).