Merge pull request #2087 from Alizter/ps/rr/fix_notations_for_8_20

fix notations for 8.20
HoTT · Sep 21, 2024 · 7566eb4 · 7566eb4
2 parents 61fbd65 + a6fc13e
commit 7566eb4
Show file tree

Hide file tree

Showing 4 changed files with 16 additions and 12 deletions.
diff --git a/theories/Basics/Notations.v b/theories/Basics/Notations.v
@@ -53,7 +53,6 @@ Reserved Notation "x * y" (at level 40, left associativity).
 Reserved Notation "x / y" (at level 40, no associativity).
 Reserved Notation "- x" (at level 35, right associativity).
 Reserved Notation "/ x" (at level 35, right associativity).
-Reserved Notation "x ^ y" (at level 30, right associativity).
 
 (** Notations for booleans *)
 
@@ -135,8 +134,10 @@ Reserved Notation "f +E g" (at level 50, left associativity).
 (** Categories *)
 Reserved Infix "-|" (at level 60, right associativity).
 Reserved Infix "<~=~>" (at level 70, no associativity).
-Reserved Notation "a // 'CAT'" (at level 1, left associativity).
-Reserved Notation "a \\ 'CAT'" (at level 1, left associativity).
+#[warnings="-postfix-notation-not-level-1"]
+Reserved Notation "a // 'CAT'" (at level 40, left associativity).
+#[warnings="-postfix-notation-not-level-1"]
+Reserved Notation "a \\ 'CAT'" (at level 40, left associativity).
 Reserved Notation "'CAT' // a" (at level 40, left associativity).
 Reserved Notation "'CAT' \\ a" (at level 40, left associativity).
 Reserved Notation "C ^op" (at level 1, format "C '^op'").
@@ -231,7 +232,8 @@ Reserved Notation "u ~~ v" (at level 30).
 Reserved Notation "! x" (at level 3, format "'!' x").
 Reserved Notation "x \\ F" (at level 40, left associativity).
 Reserved Notation "x // F" (at level 40, left associativity).
-Reserved Notation "{ { xL | xR // xcut } }" (at level 0, xR at level 39, format "{ {  xL  |  xR  //  xcut  } }").
+Reserved Notation "{ { xL | xR // xcut } }" (at level 0, xR at level 39, format "{ {  xL  |  xR // xcut  } }").
+
 Reserved Notation "x \ F" (at level 40, left associativity).
 Reserved Notation "x <> y" (at level 70, no associativity).
 Reserved Notation "x ->> y" (at level 99, right associativity, y at level 200).

diff --git a/theories/Basics/Utf8.v b/theories/Basics/Utf8.v
@@ -23,8 +23,10 @@ Reserved Notation "A 'ᵒᵖ'" (at level 1).
 Reserved Notation "A × B" (at level 40, left associativity).
 Reserved Notation "a ≤ b" (at level 70, no associativity).
 Reserved Notation "A ≃ B" (at level 85).
-Reserved Notation "a ⇓ 'CAT'" (at level 1, left associativity).
-Reserved Notation "a ⇑ 'CAT'" (at level 1, left associativity).
+#[warnings="-postfix-notation-not-level-1"]
+Reserved Notation "a ⇓ 'CAT'" (at level 40, left associativity).
+#[warnings="-postfix-notation-not-level-1"]
+Reserved Notation "a ⇑ 'CAT'" (at level 40, left associativity).
 Reserved Notation "a ≤_{ x } b" (at level 70, no associativity).
 Reserved Notation "C ↓ a" (at level 70, no associativity).
 Reserved Notation "'CAT' ⇓ a" (at level 40, left associativity).
@@ -41,7 +43,8 @@ Reserved Notation "g ∘ᴱ f" (at level 40, left associativity).
 Reserved Notation "m ≤ n" (at level 70, no associativity).
 Reserved Notation "p • q" (at level 20).
 Reserved Notation "p •' q" (at level 21, left associativity, format "'[v' p '/' '•''  q ']'").
-Reserved Notation "x ₁" (at level 1).
+#[warnings="-postfix-notation-not-level-1"]
+Reserved Notation "x ₁" (at level 10).
 Reserved Notation "x ₂" (at level 1).
 Reserved Notation "¬ x" (at level 35, right associativity).
 Reserved Notation "x ⇓ F" (at level 40, left associativity).

diff --git a/theories/Spaces/BinInt/Core.v b/theories/Spaces/BinInt/Core.v
@@ -208,8 +208,6 @@ Definition binint_pow x y :=
     | neg _ => 0
   end.
 
-Infix "^" := binint_pow : binint_scope.
-
 (** ** Square *)
 
 Definition binint_square x :=

diff --git a/theories/WildCat/Monoidal.v b/theories/WildCat/Monoidal.v
@@ -647,9 +647,10 @@ Section TwistConstruction.
   Local Infix "⊗R" := (fmap01 cat_tensor) (at level 40) : monoidal_scope.
   Local Infix "⊗L" := (fmap10 cat_tensor) (at level 40) : monoidal_scope.
   Local Notation "f ∘ g" := (f $o g) (at level 61, left associativity, format "f  '/' '∘'  g") : monoidal_scope.
-  Local Notation "f $== g :> A" := (GpdHom (A := A) f g)
-    (at level 80, format "'[v' '[v' f ']' '/'  $== '/'  '[v' g ']'  '/' :>  '[' A ']' ']'")
-    : long_path_scope.
+  (** TODO: in 8.19 this notation causes issues, when updating to 8.20 we should uncomment this. *)
+  (* Local Notation "f $== g :> A" := (GpdHom (A := A) f g)
+    (at level 70, format "'[v' '[v' f ']' '/'  $== '/'  '[v' g ']'  '/' :>  '[' A ']' ']'")
+    : long_path_scope. *)
   Local Open Scope monoidal_scope.
 
   (** [twist] is an equivalence which we will call [twiste]. *)