Use a local [rew dependent] notation

1 files changed, 12 insertions, 18 deletions

diff --git a/theories/Init/Specif.v b/theories/Init/Specif.v
index e1d8991d1..2b4cc745f 100644
--- a/theories/Init/Specif.v
+++ b/theories/Init/Specif.v
@@ -220,6 +220,12 @@ Qed.
 
 (** Equality of sigma types *)
 Import EqNotations.
+Local Notation "'rew' 'dependent' [ Q ] H 'in' H'"
+  := (match H as p in (_ = y) return Q y (rew p in _) with
+      | eq_refl => H'
+      end)
+       (at level 10, H' at level 10,
+        format "'[' 'rew'  'dependent'  [ Q ]  '/    ' H  in  '/' H' ']'").
 
 (** Equality for [sigT] *)
 Section sigT.
@@ -303,9 +309,7 @@ Section sigT.
     = existT
         (Q y)
         (rew H in projT1 u)
-        match H in (_ = y) return Q y (rew H in projT1 u) with
-          | eq_refl => projT2 u
-        end.
+        (rew dependent [Q] H in (projT2 u)).
   Proof.
     destruct H, u; reflexivity.
   Defined.
@@ -376,9 +380,7 @@ Section sig.
     = exist
         (Q y)
         (rew H in proj1_sig u)
-        match H in (_ = y) return Q y (rew H in proj1_sig u) with
-          | eq_refl => proj2_sig u
-        end.
+        (rew dependent [Q] H in proj2_sig u).
   Proof.
     destruct H, u; reflexivity.
   Defined.
@@ -492,12 +494,8 @@ Section sigT2.
         (Q y)
         (R y)
         (rew H in projT1 u)
-        match H in (_ = y) return Q y (rew H in projT1 u) with
-          | eq_refl => projT2 u
-        end
-        match H in (_ = y) return R y (rew H in projT1 u) with
-          | eq_refl => projT3 u
-        end.
+        (rew dependent [Q] H in projT2 u)
+        (rew dependent [R] H in projT3 u).
   Proof.
     destruct H, u; reflexivity.
   Defined.
@@ -611,12 +609,8 @@ Section sig2.
         (Q y)
         (R y)
         (rew H in proj1_sig u)
-        match H in (_ = y) return Q y (rew H in proj1_sig u) with
-          | eq_refl => proj2_sig u
-        end
-        match H in (_ = y) return R y (rew H in proj1_sig u) with
-          | eq_refl => proj3_sig u
-        end.
+        (rew dependent [Q] H in proj2_sig u)
+        (rew dependent [R] H in proj3_sig u).
   Proof.
     destruct H, u; reflexivity.
   Defined.