solved issue related to level 0 bi-closed notations

uds-psl · Jan 21, 2025 · 10478ab · 10478ab
1 parent 7b03998
commit 10478ab
Show file tree

Hide file tree

Showing 6 changed files with 10 additions and 10 deletions.
diff --git a/theories/H10/Dio/dio_logic.v b/theories/H10/Dio/dio_logic.v
@@ -95,7 +95,7 @@ Local Notation "x ≐ y ⨢ z" := (df_add x y z)
 Local Notation "x ≐ y ⨰ z" := (df_mul x y z) 
       (at level 49, no associativity, y at next level, format "x  ≐  y  ⨰  z").
 
-Local Reserved Notation "'⟦' t '⟧'" (at level 1, format "⟦ t ⟧").
+Local Reserved Notation "'⟦' t '⟧'" (at level 0, format "⟦ t ⟧").
 Local Reserved Notation "f '⦃' σ '⦄'" (at level 1, format "f ⦃ σ ⦄").
 
 Section diophantine_logic_basics.

diff --git a/theories/ILL/Ll/ill.v b/theories/ILL/Ll/ill.v
@@ -143,7 +143,7 @@ Section trivial_phase_semantics.
 
   Variables (n : nat) (s : ill_vars -> vec nat n -> Prop).
 
-  Reserved Notation "'⟦' A '⟧'" (at level 65).
+  Reserved Notation "'⟦' A '⟧'" (at level 0).
 
   Definition ill_tps_imp (X Y : _ -> Prop) (v : vec _ n) := forall x, X x -> Y (vec_plus x v).
   Definition ill_tps_mult (X Y : _ -> Prop) (x : vec _ n) := exists a b, x = vec_plus a b /\ X a /\ Y b. 

diff --git a/theories/ILL/Ll/ill_cll.v b/theories/ILL/Ll/ill_cll.v
@@ -20,8 +20,8 @@ Section mapping_ill_to_cll.
 
   (* Syntatic translations from/to ILL and CLL formulas *)
 
-  Reserved Notation "[ f ]" (at level 1).
-  Reserved Notation "⟨ f ⟩" (at level 1).
+  Reserved Notation "[ f ]" (at level 0).
+  Reserved Notation "⟨ f ⟩" (at level 0).
 
   Fixpoint ill_cll f :=
     match f with

diff --git a/theories/ILL/Ll/imsell.v b/theories/ILL/Ll/imsell.v
@@ -23,7 +23,7 @@ Local Infix "~p" := (@Permutation _) (at level 70).
 Local Notation "X ⊆ Y" := (forall a, X a -> Y a : Prop) (at level 70).
 Local Infix "∊" := In (at level 70).
 
-Local Reserved Notation "'⟦' A '⟧'" (at level 1, format "⟦ A ⟧").
+Local Reserved Notation "'⟦' A '⟧'" (at level 0, format "⟦ A ⟧").
 
 Section IMSELL.
 
@@ -158,7 +158,7 @@ Section IMSELL.
         * intros ->; auto.
     Qed.
 
-    Reserved Notation "⟪ Γ ⟫" (at level 1, format "⟪ Γ ⟫").
+    Reserved Notation "⟪ Γ ⟫" (at level 0, format "⟪ Γ ⟫").
 
     Fixpoint imsell_tps_list Γ :=
       match Γ with
@@ -208,7 +208,7 @@ Section IMSELL.
 
     Definition imsell_sequent_tps Γ A := ⟪Γ⟫ -⊛ ⟦A⟧.
 
-    Notation "'[<' Γ '|-' A '>]'" := (imsell_sequent_tps Γ A) (at level 1, format "[<  Γ  |-  A  >]").
+    Notation "'[<' Γ '|-' A '>]'" := (imsell_sequent_tps Γ A) (at level 0, format "[<  Γ  |-  A  >]").
 
     Fact imsell_sequent_tps_mono Γ A B :
            ⟦A⟧ ⊆ ⟦B⟧ -> [< Γ |- A >] ⊆ [< Γ |- B >].

diff --git a/theories/ILL/Reductions/ndMM2_IMSELL.v b/theories/ILL/Reductions/ndMM2_IMSELL.v
@@ -27,7 +27,7 @@ Local Infix "~p" := (@Permutation _) (at level 70).
 Local Notation "X ⊆ Y" := (forall a, X a -> Y a : Prop) (at level 70).
 Local Infix "∊" := In (at level 70).
 
-Local Reserved Notation "'⟦' A '⟧'" (at level 1, format "⟦ A ⟧").
+Local Reserved Notation "'⟦' A '⟧'" (at level 0, format "⟦ A ⟧").
 
 Local Fact pair_plus x1 y1 x2 y2 : 
           vec_plus (x1##y1##vec_nil) (x2##y2##vec_nil) 

diff --git a/theories/MinskyMachines/Reductions/MMA2_to_ndMM2_ACCEPT.v b/theories/MinskyMachines/Reductions/MMA2_to_ndMM2_ACCEPT.v
@@ -41,7 +41,7 @@ Section MMA2_ndMM2.
   Definition pos2_to_bool (p : pos 2) :=
     match p with pos0 => α | _ => β end.
 
-  Notation "⌈ p ⌉" := (pos2_to_bool p) (at level 1, format "⌈ p ⌉").
+  Notation "⌈ p ⌉" := (pos2_to_bool p) (at level 0, format "⌈ p ⌉").
 
   Definition mma2_instr_enc i (ρ : mm_instr (pos 2)) :=
     match ρ with
@@ -51,7 +51,7 @@ Section MMA2_ndMM2.
 
   Notation "'⟨' i , ρ '⟩₁'" := (mma2_instr_enc i  ρ) (format "⟨ i , ρ ⟩₁").
 
-  Reserved Notation "'⟪' i , l '⟫ₗ'" (at level 1, format "⟪ i , l ⟫ₗ").
+  Reserved Notation "'⟪' i , l '⟫ₗ'" (at level 0, format "⟪ i , l ⟫ₗ").
 
   Fixpoint mma2_linstr_enc i l :=
     match l with