Only parsing in Reserved Notation: turning notice into a warning.

2 files changed, 8 insertions, 8 deletions

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 ']'").