From 6d3c5956ee7c56c816750f3879a5ddafcdf81f0f Mon Sep 17 00:00:00 2001
From: Jason Gross <jgross@mit.edu>
Date: Tue, 21 Feb 2017 20:42:52 -0500
Subject: Use [rew_] instead of [eq_rect_] prefix

As per Hugo's request.
---
 theories/Init/Logic.v  |  4 ++--
 theories/Init/Specif.v | 14 +++++++-------
 2 files changed, 9 insertions(+), 9 deletions(-)

(limited to 'theories/Init')

diff --git a/theories/Init/Logic.v b/theories/Init/Logic.v
index 1f94f7586..b5d99aac6 100644
--- a/theories/Init/Logic.v
+++ b/theories/Init/Logic.v
@@ -673,7 +673,7 @@ Section ex.
     : ex_intro P u1 u2 = ex_intro P v1 v2
     := 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)
+  Lemma rew_ex {A x} {P : A -> Type} (Q : forall a, P a -> Prop) (u : ex (Q x)) {y} (H : x = y)
   : rew [fun a => ex (Q a)] H in u
     = match u with
         | ex_intro _ u1 u2
@@ -720,7 +720,7 @@ Section ex2.
     : ex_intro2 P Q u1 u2 u3 = ex_intro2 P Q v1 v2 v3
     := eq_ex2' u1 v1 u2 v2 u3 v3 p (P_hprop _ _ _) (Q_hprop _ _ _).
 
-  Lemma eq_rect_ex2 {A x} {P : A -> Type}
+  Lemma rew_ex2 {A x} {P : A -> Type}
         (Q : forall a, P a -> Prop)
         (R : forall a, P a -> Prop)
         (u : ex2 (Q x) (R x)) {y} (H : x = y)
diff --git a/theories/Init/Specif.v b/theories/Init/Specif.v
index 1d8a40ebb..f3570b0d6 100644
--- a/theories/Init/Specif.v
+++ b/theories/Init/Specif.v
@@ -289,10 +289,10 @@ Section sigT.
   Definition eq_sigT_nondep {A B : Type} (u v : @sigT A (fun _ => B))
              (p : projT1 u = projT1 v) (q : projT2 u = projT2 v)
   : u = v
-    := @eq_sigT _ _ u v p (eq_trans (eq_rect_const _ _) q).
+    := @eq_sigT _ _ u v p (eq_trans (rew_const _ _) q).
 
   (** Classification of transporting across an equality of [sigT]s *)
-  Lemma eq_rect_sigT {A x} {P : A -> Type} (Q : forall a, P a -> Prop) (u : sigT (Q x)) {y} (H : x = y)
+  Lemma rew_sigT {A x} {P : A -> Type} (Q : forall a, P a -> Prop) (u : sigT (Q x)) {y} (H : x = y)
   : rew [fun a => sigT (Q a)] H in u
     = existT
         (Q y)
@@ -358,7 +358,7 @@ Section sig.
     : u = v <-> (proj1_sig u = proj1_sig v)
     := conj (fun p => f_equal (@proj1_sig _ _) p) (eq_sig_hprop P_hprop u v).
 
-  Lemma eq_rect_sig {A x} {P : A -> Type} (Q : forall a, P a -> Prop) (u : sig (Q x)) {y} (H : x = y)
+  Lemma rew_sig {A x} {P : A -> Type} (Q : forall a, P a -> Prop) (u : sig (Q x)) {y} (H : x = y)
   : rew [fun a => sig (Q a)] H in u
     = exist
         (Q y)
@@ -460,10 +460,10 @@ Section sigT2.
   Definition eq_sigT2_nondep {A B C : Type} (u v : @sigT2 A (fun _ => B) (fun _ => C))
              (p : projT1 u = projT1 v) (q : projT2 u = projT2 v) (r : projT3 u = projT3 v)
   : u = v
-    := @eq_sigT2 _ _ _ u v p (eq_trans (eq_rect_const _ _) q) (eq_trans (eq_rect_const _ _) r).
+    := @eq_sigT2 _ _ _ u v p (eq_trans (rew_const _ _) q) (eq_trans (rew_const _ _) r).
 
   (** Classification of transporting across an equality of [sigT2]s *)
-  Lemma eq_rect_sigT2 {A x} {P : A -> Type} (Q R : forall a, P a -> Prop)
+  Lemma rew_sigT2 {A x} {P : A -> Type} (Q R : forall a, P a -> Prop)
         (u : sigT2 (Q x) (R x))
         {y} (H : x = y)
   : rew [fun a => sigT2 (Q a) (R a)] H in u
@@ -571,10 +571,10 @@ Section sig2.
   Definition eq_sig2_nondep {A} {B C : Prop} (u v : @sig2 A (fun _ => B) (fun _ => C))
              (p : proj1_sig u = proj1_sig v) (q : proj2_sig u = proj2_sig v) (r : proj3_sig u = proj3_sig v)
   : u = v
-    := @eq_sig2 _ _ _ u v p (eq_trans (eq_rect_const _ _) q) (eq_trans (eq_rect_const _ _) r).
+    := @eq_sig2 _ _ _ u v p (eq_trans (rew_const _ _) q) (eq_trans (rew_const _ _) r).
 
   (** Classification of transporting across an equality of [sig2]s *)
-  Lemma eq_rect_sig2 {A x} {P : A -> Type} (Q R : forall a, P a -> Prop)
+  Lemma rew_sig2 {A x} {P : A -> Type} (Q R : forall a, P a -> Prop)
         (u : sig2 (Q x) (R x))
         {y} (H : x = y)
   : rew [fun a => sig2 (Q a) (R a)] H in u
-- 
cgit v1.2.3