change priority for £ letting Coq decide for itself

uds-psl · Jan 23, 2025 · a1c59db · a1c59db
1 parent 6662d6f
commit a1c59db
Show file tree

Hide file tree

Showing 3 changed files with 3 additions and 3 deletions.
diff --git 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
@@ -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
@@ -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)).