Fix notation

mattam82 · May 17, 2024 · 2fab4b7 · 2fab4b7
1 parent 05651e1
commit 2fab4b7
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/theories/Init.v b/theories/Init.v
@@ -89,8 +89,8 @@ Notation "( x , .. , y , z )" :=
       (right associativity, at level 0,
        format "( x ,  .. ,  y ,  z )") : equations_scope.
 
-Notation " x .1 " := (pr1 x) (at level 3, format "x .1") : equations_scope.
-Notation " x .2 " := (pr2 x) (at level 3, format "x .2") : equations_scope.
+Notation " x .1 " := (pr1 x) : equations_scope.
+Notation " x .2 " := (pr2 x) : equations_scope.
 
 End Sigma_Notations.