From 954a125f4470cf7d723cd78b003a4cf8c17ca3f6 Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Mon, 5 Dec 2016 11:05:02 -0500
Subject: Use [rew] notations rather than [eq_rect]

As per Hugo's request in
https://github.com/coq/coq/pull/384#issuecomment-264891011
---
 theories/Init/Logic.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/theories/Init/Logic.v b/theories/Init/Logic.v
index 437d802d83..12ec9dd775 100644
--- a/theories/Init/Logic.v
+++ b/theories/Init/Logic.v
@@ -528,13 +528,13 @@ reflexivity.
 Defined.
 
 Lemma eq_trans_eq_rect_distr : forall A (P:A -> Type) (x y z:A) (e:x=y) (e':y=z) (k:P x),
-    eq_rect _ P k _ (eq_trans e e') = eq_rect _ P (eq_rect _ P k _ e) _ e'.
+    rew (eq_trans e e') in k = rew e' in rew e in k.
 Proof.
   destruct e, e'; reflexivity.
 Defined.
 
 Lemma eq_rect_const : forall A P (x y:A) (e:x=y) (k:P),
-    eq_rect _ (fun _ : A => P) k _ e = k.
+    rew [fun _ => P] e in k = k.
 Proof.
   destruct e; reflexivity.
 Defined.
-- 
cgit v1.2.3