diff --git a/theories/ILL/CLL.v b/theories/ILL/CLL.v
index 19480f84..a6ad464f 100644
--- a/theories/ILL/CLL.v
+++ b/theories/ILL/CLL.v
@@ -33,7 +33,7 @@ Inductive cll_form : Set :=
 
 (* Variables *)
 
-Notation "'£' x" := (cll_var x) (at level 1).
+Notation "£" := cll_var.
 
 (* Constants *)
 
diff --git a/theories/ILL/Ll/imsell.v b/theories/ILL/Ll/imsell.v
index c86d7bcb..6b5bdb3e 100644
--- a/theories/ILL/Ll/imsell.v
+++ b/theories/ILL/Ll/imsell.v
@@ -29,7 +29,7 @@ Section IMSELL.
 
   Variable bang : Type.
 
-  Notation "£ A" := (@imsell_var _ _ A) (at level 1).
+  Notation "£" := (@imsell_var _ _).
   Notation "‼ l" := (@imsell_lban nat bang l).
 
   Fact imsell_lban_perm Σ Γ : Σ ~p Γ -> ‼Σ ~p ‼Γ.
diff --git a/theories/ILL/Reductions/ndMM2_IMSELL.v b/theories/ILL/Reductions/ndMM2_IMSELL.v
index bb01e9c7..7cc4a78d 100644
--- a/theories/ILL/Reductions/ndMM2_IMSELL.v
+++ b/theories/ILL/Reductions/ndMM2_IMSELL.v
@@ -66,7 +66,7 @@ Section ndmm2_imsell.
 
   Hint Resolve Hai Hbi Ha Hb Hi Hab Hba bang_le_refl bang_U_clos : core.
 
-  Notation "£ A" := (@imsell_var _ _ A) (at level 1).
+  Notation "£" := (@imsell_var _ _).
   Notation "‼ l" := (@imsell_lban nat sig l).
   Notation "‼∞" := (map (fun A => ![∞]A)).