Use [rew] notations rather than [eq_rect]

As per Hugo's suggestion in
https://github.com/coq/coq/pull/384#issuecomment-264891011

1 files changed, 5 insertions, 5 deletions

diff --git a/theories/Init/Logic.v b/theories/Init/Logic.v
index 968922737..b855154ac 100644
--- a/theories/Init/Logic.v
+++ b/theories/Init/Logic.v
@@ -654,7 +654,7 @@ Declare Right Step iff_trans.
 Section ex.
   Local Unset Implicit Arguments.
   Definition eq_ex_uncurried' {A : Type} (P : A -> Prop) {u1 v1 : A} {u2 : P u1} {v2 : P v1}
-             (pq : exists p : u1 = v1, eq_rect _ _ u2 _ p = v2)
+             (pq : exists p : u1 = v1, rew p in u2 = v2)
   : ex_intro P u1 u2 = ex_intro P v1 v2.
   Proof.
     destruct pq as [p q].
@@ -663,7 +663,7 @@ Section ex.
   Defined.
 
   Definition eq_ex' {A : Type} {P : A -> Prop} (u1 v1 : A) (u2 : P u1) (v2 : P v1)
-             (p : u1 = v1) (q : eq_rect _ _ u2 _ p = v2)
+             (p : u1 = v1) (q : rew p in u2 = v2)
   : ex_intro P u1 u2 = ex_intro P v1 v2
     := eq_ex_uncurried' P (ex_intro _ p q).
 
@@ -674,13 +674,13 @@ Section ex.
     := eq_ex' u1 v1 u2 v2 p (P_hprop _ _ _).
 
   Lemma eq_rect_ex {A x} {P : A -> Type} (Q : forall a, P a -> Prop) (u : ex (Q x)) {y} (H : x = y)
-  : eq_rect x (fun a => ex (Q a)) u y H
+  : rew [fun a => ex (Q a)] H in u
     = match u with
         | ex_intro _ u1 u2
           => ex_intro
                (Q y)
-               (eq_rect x P u1 y H)
-               match H in (_ = y) return Q y (eq_rect x P u1 y H) with
+               (rew H in u1)
+               match H in (_ = y) return Q y (rew H in u1) with
                  | eq_refl => u2
                end
       end.