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

1 files changed, 8 insertions, 6 deletions

diff --git a/theories/Init/Logic.v b/theories/Init/Logic.v
index 00a93efa0..fe3f947da 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)