Adapt to coq/coq#18224

mattam82 · Nov 10, 2023 · a2b612a · a2b612a
1 parent dbc5fbb
commit a2b612a
Show file tree

Hide file tree

Showing 3 changed files with 7 additions and 7 deletions.
diff --git a/examples/definterp.v b/examples/definterp.v
@@ -42,8 +42,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.
 
 Local Open Scope equations_scope.
 

diff --git a/examples/polynomials.v b/examples/polynomials.v
@@ -340,8 +340,8 @@ Definition apoly {n b} := existT (fun b => poly b n) b.
     one case to inject an integer into a polynomial and in the
     [poly_s], [poly_s] case to inspect a recursive call. *)
 
-Notation " x .1 " := (projT1 x) (at level 3, format "x .1").
-Notation " x .2 " := (projT2 x) (at level 3, format "x .2").
+Notation " x .1 " := (projT1 x).
+Notation " x .2 " := (projT2 x).
 
 Equations plus {n} {b1} (p1 : poly b1 n) {b2} (p2 : poly b2 n) : { b : bool & poly b n } :=
   plus poly_z        poly_z          := apoly poly_z;

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.
 
@@ -166,4 +166,4 @@ Ltac unfold_recursor := fail "Equations.Init.unfold_recursor has not been bound
 Ltac unfold_recursor_ext := fail "Equations.Init.unfold_recursor_ext has not been bound yet".
 
 (** Forward reference to an internal tactic to combine eliminators for mutual and nested definitions *)
-Ltac specialize_mutfix := fail "Equations.Init.specialize_mutfix has not been bound yet".
+Ltac specialize_mutfix := fail "Equations.Init.specialize_mutfix has not been bound yet".