Move reservation of notations .1 and .2 from ssr to Init

Also move them from level 2 to level 1 in preparation of removal of camlp5 recovery mechanism.
coq · Oct 30, 2023 · 7861b99 · 7861b99
1 parent bda17b6
commit 7861b99
Show file tree

Hide file tree

Showing 2 changed files with 5 additions and 2 deletions.
diff --git a/theories/Init/Notations.v b/theories/Init/Notations.v
@@ -114,6 +114,11 @@ Notation "'if' c 'is' p 'then' u 'else' v" :=
 
 End IfNotations.
 
+(** Notations for first and second projections *)
+
+Reserved Notation "p .1" (at level 1, left associativity, format "p .1").
+Reserved Notation "p .2" (at level 1, left associativity, format "p .2").
+
 (** Scopes *)
 
 Declare Scope core_scope.

diff --git a/theories/ssr/ssrfun.v b/theories/ssr/ssrfun.v
@@ -225,8 +225,6 @@ Unset Strict Implicit.
 Unset Printing Implicit Defensive.
 
 (** Parsing / printing declarations. *)
-Reserved Notation "p .1" (at level 2, left associativity, format "p .1").
-Reserved Notation "p .2" (at level 2, left associativity, format "p .2").
 Reserved Notation "f ^~ y" (at level 10, y at level 8, no associativity,
   format "f ^~  y").
 Reserved Notation "@^~ x" (at level 10, x at level 8, no associativity,