diff --git a/examples/definterp.v b/examples/definterp.v
index 43eece3b..1acbbb96 100644
--- 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
index d303d37e..5a30721a 100644
--- a/examples/polynomials.v
+++ b/examples/polynomials.v
@@ -339,8 +339,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
index 70cc1d79..fecdff85 100644
--- 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".
\ No newline at end of file
+Ltac specialize_mutfix := fail "Equations.Init.specialize_mutfix has not been bound yet".