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, 3 insertions, 2 deletions

diff --git a/theories/Vectors/VectorDef.v b/theories/Vectors/VectorDef.v
index 9129b94de..ad241462e 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).