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, 6 insertions, 4 deletions

diff --git a/theories/Logic/EqdepFacts.v b/theories/Logic/EqdepFacts.v
index 8fbd79fa4..a341a7a5a 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.