Add rew dependent Notations

This way when users `Import EqNotations`, we get pretty-printing for
equality `match` statements too.

1 files changed, 52 insertions, 7 deletions

diff --git a/theories/Init/Logic.v b/theories/Init/Logic.v
index 4d84d61f9f..8ba17e38c8 100644
--- a/theories/Init/Logic.v
+++ b/theories/Init/Logic.v
@@ -460,6 +460,58 @@ Module EqNotations.
   Notation "'rew' -> [ P ] H 'in' H'" := (eq_rect _ P H' _ H)
     (at level 10, H' at level 10, only parsing).
 
+  Notation "'rew' 'dependent' H 'in' H'"
+    := (match H with
+        | eq_refl => H'
+        end)
+         (at level 10, H' at level 10,
+          format "'[' 'rew'  'dependent'  H  in  '/' H' ']'").
+  Notation "'rew' 'dependent' -> H 'in' H'"
+    := (match H with
+        | eq_refl => H'
+        end)
+         (at level 10, H' at level 10, only parsing).
+  Notation "'rew' 'dependent' <- H 'in' H'"
+    := (match eq_sym H with
+        | eq_refl => H'
+        end)
+         (at level 10, H' at level 10,
+          format "'[' 'rew'  'dependent'  <-  H  in  '/' H' ']'").
+  Notation "'rew' 'dependent' [ 'fun' y p => P ] H 'in' H'"
+    := (match H as p in (_ = y) return P with
+        | eq_refl => H'
+        end)
+         (at level 10, H' at level 10, y ident, p ident,
+          format "'[' 'rew'  'dependent'  [ 'fun'  y  p  =>  P ]  '/    ' H  in  '/' H' ']'").
+  Notation "'rew' 'dependent' -> [ 'fun' y p => P ] H 'in' H'"
+    := (match H as p in (_ = y) return P with
+        | eq_refl => H'
+        end)
+         (at level 10, H' at level 10, y ident, p ident, only parsing).
+  Notation "'rew' 'dependent' <- [ 'fun' y p => P ] H 'in' H'"
+    := (match eq_sym H as p in (_ = y) return P with
+        | eq_refl => H'
+        end)
+         (at level 10, H' at level 10, y ident, p ident,
+          format "'[' 'rew'  'dependent'  <-  [ 'fun'  y  p  =>  P ]  '/    ' H  in  '/' H' ']'").
+  Notation "'rew' 'dependent' [ P ] H 'in' H'"
+    := (match H as p in (_ = y) return P y p with
+        | eq_refl => H'
+        end)
+         (at level 10, H' at level 10,
+          format "'[' 'rew'  'dependent'  [ P ]  '/    ' H  in  '/' H' ']'").
+  Notation "'rew' 'dependent' -> [ P ] H 'in' H'"
+    := (match H as p in (_ = y) return P y p with
+        | eq_refl => H'
+        end)
+         (at level 10, H' at level 10,
+          only parsing).
+  Notation "'rew' 'dependent' <- [ P ] H 'in' H'"
+    := (match eq_sym H as p in (_ = y) return P y p with
+        | eq_refl => H'
+        end)
+         (at level 10, H' at level 10,
+          format "'[' 'rew'  'dependent'  <-  [ P ]  '/    ' H  in  '/' H' ']'").
 End EqNotations.
 
 Import EqNotations.
@@ -793,13 +845,6 @@ Qed.
 Declare Left Step iff_stepl.
 Declare Right Step iff_trans.
 
-Local Notation "'rew' 'dependent' H 'in' H'"
-  := (match H with
-      | eq_refl => H'
-      end)
-       (at level 10, H' at level 10,
-        format "'[' 'rew'  'dependent'  '/    ' H  in  '/' H' ']'").
-
 (** Equality for [ex] *)
 Section ex.
   Local Unset Implicit Arguments.