diff --git a/theories/cauchyreals.v b/theories/cauchyreals.v
index b919860..2059e59 100644
--- a/theories/cauchyreals.v
+++ b/theories/cauchyreals.v
@@ -628,7 +628,7 @@ Lemma cst_crealP (x : F) : creal_axiom (fun _ => x).
 Proof. by exists (fun _ => 0%N)=> *; rewrite subrr normr0. Qed.
 Definition cst_creal (x : F) := CReal (cst_crealP x).
 Notation "x %:CR" := (cst_creal x)
-  (at level 2, left associativity, format "x %:CR") : creal_scope.
+  (at level 1, left associativity, format "x %:CR") : creal_scope.
 Notation "0" := (0 %:CR) : creal_scope.
 
 Lemma lbound0P (x : creal) (x_neq0 : x != 0) i :
@@ -1638,7 +1638,7 @@ Notation "!=%CR" := neq_creal : creal_scope.
 Notation "x != y" := (neq_creal x  y) : creal_scope.
 
 Notation "x %:CR" := (cst_creal x)
-  (at level 2, left associativity, format "x %:CR") : creal_scope.
+  (at level 1, left associativity, format "x %:CR") : creal_scope.
 Notation "0" := (0 %:CR)%CR : creal_scope.
 
 Notation "<%CR" := lt_creal : creal_scope.
diff --git a/theories/complex.v b/theories/complex.v
index e9b19af..00efb60 100644
--- a/theories/complex.v
+++ b/theories/complex.v
@@ -30,7 +30,7 @@ Reserved Notation "x +i* y"
 Reserved Notation "x -i* y"
   (at level 40, left associativity, format "x  -i*  y").
 Reserved Notation "R [i]"
-  (at level 2, left associativity, format "R [i]").
+  (at level 1, left associativity, format "R [i]").
 
 Local Notation sgr := Num.sg.
 Local Notation sqrtr := Num.sqrt.
diff --git a/theories/realalg.v b/theories/realalg.v
index 7b930de..667b7cb 100644
--- a/theories/realalg.v
+++ b/theories/realalg.v
@@ -571,7 +571,7 @@ Definition to_alg_def (phF : phant F) : F -> alg :=
   lift_embed alg cst_algcreal.
 Notation to_alg := (@to_alg_def (Phant F)).
 Notation "x %:RA" := (to_alg x)
-  (at level 2, left associativity, format "x %:RA").
+  (at level 1, left associativity, format "x %:RA").
 Local Notation "p ^ f" := (map_poly f p) : ring_scope.
 
 Canonical to_alg_pi_morph := PiEmbed to_alg.
@@ -1176,7 +1176,7 @@ End RealAlg.
 
 Notation to_alg F := (@to_alg_def _ (Phant F)).
 Notation "x %:RA" := (to_alg _ x)
-  (at level 2, left associativity, format "x %:RA").
+  (at level 1, left associativity, format "x %:RA").
 
 Lemma upper_nthrootVP (F : archiFieldType) (x : F) (i : nat) :
    0 < x -> (Num.bound (x ^-1) <= i)%N -> 2%:R ^- i < x.
@@ -1381,7 +1381,7 @@ Notation "{ 'realclosure'  F }" := (RealAlg.alg F).
 Notation annul_realalg := RealAlg.annul_alg.
 Notation realalg_of F := (@RealAlg.to_alg_def _ (Phant F)).
 Notation "x %:RA" := (realalg_of x)
-  (at level 2, left associativity, format "x %:RA").
+  (at level 1, left associativity, format "x %:RA").
 
 HB.instance Definition _ (F : archiFieldType) := GRing.RMorphism.on (to_alg F).