From 1916fc22a187bdaaad4c99fa00f345c6f7314a73 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 13 Feb 2020 00:54:32 +0100
Subject: Choosing a standard format for the "rew dependent" notation.

---
 theories/Init/Logic.v  | 4 ++--
 theories/Init/Specif.v | 6 ------
 2 files changed, 2 insertions(+), 8 deletions(-)

diff --git a/theories/Init/Logic.v b/theories/Init/Logic.v
index 8ba17e38c8..9698737d33 100644
--- a/theories/Init/Logic.v
+++ b/theories/Init/Logic.v
@@ -465,7 +465,7 @@ Module EqNotations.
         | eq_refl => H'
         end)
          (at level 10, H' at level 10,
-          format "'[' 'rew'  'dependent'  H  in  '/' H' ']'").
+          format "'[' 'rew'  'dependent'  '/    ' H  in  '/' H' ']'").
   Notation "'rew' 'dependent' -> H 'in' H'"
     := (match H with
         | eq_refl => H'
@@ -476,7 +476,7 @@ Module EqNotations.
         | eq_refl => H'
         end)
          (at level 10, H' at level 10,
-          format "'[' 'rew'  'dependent'  <-  H  in  '/' H' ']'").
+          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'
diff --git a/theories/Init/Specif.v b/theories/Init/Specif.v
index c00f8edcf7..d3e5ddcc8a 100644
--- a/theories/Init/Specif.v
+++ b/theories/Init/Specif.v
@@ -255,12 +255,6 @@ Qed.
 (** Equality of sigma types *)
 
 Import EqNotations.
-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 [sigT] *)
 Section sigT.
-- 
cgit v1.2.3