Merge PR #10832: Addressing #6082 and #7766: warning when overriding notation format + new notion of format associated to a given interpretation

Ack-by: maximedenes

4 files changed, 10 insertions, 16 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.
diff --git a/theories/ssr/ssrbool.v b/theories/ssr/ssrbool.v
index 475859fcc2..e2ab812cce 100644
--- a/theories/ssr/ssrbool.v
+++ b/theories/ssr/ssrbool.v
@@ -437,7 +437,7 @@ Reserved Notation "{ 'on' cd , 'bijective' f }" (at level 0, f at level 8,
  is | or => . It is important that in other notations a leading square
  bracket #[# is always followed by an operator symbol or a fixed identifier.   **)
 
-Reserved Notation "[ /\ P1 & P2 ]" (at level 0, only parsing).
+Reserved Notation "[ /\ P1 & P2 ]" (at level 0).
 Reserved Notation "[ /\ P1 , P2 & P3 ]" (at level 0, format
   "'[hv' [ /\ '['  P1 , '/'  P2 ']' '/ '  &  P3 ] ']'").
 Reserved Notation "[ /\ P1 , P2 , P3 & P4 ]" (at level 0, format
@@ -445,21 +445,21 @@ Reserved Notation "[ /\ P1 , P2 , P3 & P4 ]" (at level 0, format
 Reserved Notation "[ /\ P1 , P2 , P3 , P4 & P5 ]" (at level 0, format
   "'[hv' [ /\ '['  P1 , '/'  P2 , '/'  P3 , '/'  P4 ']' '/ '  &  P5 ] ']'").
 
-Reserved Notation "[ \/ P1 | P2 ]" (at level 0, only parsing).
+Reserved Notation "[ \/ P1 | P2 ]" (at level 0).
 Reserved Notation "[ \/ P1 , P2 | P3 ]" (at level 0, format
   "'[hv' [ \/ '['  P1 , '/'  P2 ']' '/ '  |  P3 ] ']'").
 Reserved Notation "[ \/ P1 , P2 , P3 | P4 ]" (at level 0, format
   "'[hv' [ \/ '['  P1 , '/'  P2 , '/'  P3 ']' '/ '  |  P4 ] ']'").
 
-Reserved Notation "[ && b1 & c ]" (at level 0, only parsing).
+Reserved Notation "[ && b1 & c ]" (at level 0).
 Reserved Notation "[ && b1 , b2 , .. , bn & c ]" (at level 0, format
   "'[hv' [ && '['  b1 , '/'  b2 , '/'  .. , '/'  bn ']' '/ '  &  c ] ']'").
 
-Reserved Notation "[ || b1 | c ]" (at level 0, only parsing).
+Reserved Notation "[ || b1 | c ]" (at level 0).
 Reserved Notation "[ || b1 , b2 , .. , bn | c ]" (at level 0, format
   "'[hv' [ || '['  b1 , '/'  b2 , '/'  .. , '/'  bn ']' '/ '  |  c ] ']'").
 
-Reserved Notation "[ ==> b1 => c ]" (at level 0, only parsing).
+Reserved Notation "[ ==> b1 => c ]" (at level 0).
 Reserved Notation "[ ==> b1 , b2 , .. , bn => c ]" (at level 0, format
   "'[hv' [ ==> '['  b1 , '/'  b2 , '/'  .. , '/'  bn ']' '/'  =>  c ] ']'").
 
diff --git a/theories/ssr/ssreflect.v b/theories/ssr/ssreflect.v
index bc4a57dedd..701ebcad56 100644
--- a/theories/ssr/ssreflect.v
+++ b/theories/ssr/ssreflect.v
@@ -97,11 +97,11 @@ Local Notation CoqCast x T := (x : T) (only parsing).
 
 (** Reserve notation that introduced in this file. **)
 Reserved Notation "'if' c 'then' vT 'else' vF" (at level 200,
-  c, vT, vF at level 200, only parsing).
+  c, vT, vF at level 200).
 Reserved Notation "'if' c 'return' R 'then' vT 'else' vF" (at level 200,
-  c, R, vT, vF at level 200, only parsing).
+  c, R, vT, vF at level 200).
 Reserved Notation "'if' c 'as' x 'return' R 'then' vT 'else' vF" (at level 200,
-  c, R, vT, vF at level 200, x ident, only parsing).
+  c, R, vT, vF at level 200, x ident).
 
 Reserved Notation "x : T" (at level 100, right associativity,
   format "'[hv' x '/ '  :  T ']'").