Dealing with -notation-overridden compile option (#231)

* solved issues wrt overridden notations in the ILL/... sub-folders
introducing modules for making notations more local.

* revert the -notation-overridden compile option to active state

* TM and SOL no warnings

---------

Co-authored-by: Andrej Dudenhefner <mrhaandi@gmail.com>

theories/ILL/CLL.v

@@ -31,42 +31,47 @@ Inductive cll_form : Set :=
 
 (* These notations replace the ILL notations *)
 
-(* Variables *)
+Module CLL_notations.
 
-Notation "£" := cll_var.
+  (* Variables *)
 
-(* Constants *)
+  Notation "£" := cll_var.
 
-Notation "⟙" := (cll_cst cll_top).
-Notation "⟘" := (cll_cst cll_bot).
-Notation "𝟙" := (cll_cst cll_1).
-Notation "𝟘" := (cll_cst cll_0).
+  (* Constants *)
 
-(* Unary connectives: linear negation and modalities *)
-(* ? cannot be used because it is reserved by Coq so we use ‽ instead *)
+  Notation "⟙" := (cll_cst cll_top).
+  Notation "⟘" := (cll_cst cll_bot).
+  Notation "𝟙" := (cll_cst cll_1).
+  Notation "𝟘" := (cll_cst cll_0).
 
-Notation "'⊖' x" := (cll_una cll_neg x) (at level 50, format "⊖ x").
-Notation "'!' x" := (cll_una cll_bang x) (at level 52).
-Notation "'‽' x" := (cll_una cll_qmrk x) (at level 52).
+  (* Unary connectives: linear negation and modalities *)
+  (* ? cannot be used because it is reserved by Coq so we use ‽ instead *)
 
-(* Binary connectives *)
+  Notation "'⊖' x" := (cll_una cll_neg x) (at level 50, format "⊖ x").
+  Notation "'!' x" := (cll_una cll_bang x) (at level 52).
+  Notation "'‽' x" := (cll_una cll_qmrk x) (at level 52).
 
-Infix "&" := (cll_bin cll_with) (at level 50).
-Infix "⅋" := (cll_bin cll_par) (at level 50).
-Infix "⊗" := (cll_bin cll_times) (at level 50).
-Infix "⊕" := (cll_bin cll_plus) (at level 50).
-Infix "⊸" := (cll_bin cll_limp) (at level 51, right associativity).
+  (* Binary connectives *)
 
-(* Modalities iterated over lists *)
+  Infix "&" := (cll_bin cll_with) (at level 50).
+  Infix "⅋" := (cll_bin cll_par) (at level 50).
+  Infix "⊗" := (cll_bin cll_times) (at level 50).
+  Infix "⊕" := (cll_bin cll_plus) (at level 50).
+  Infix "⊸" := (cll_bin cll_limp) (at level 51, right associativity).
 
-Notation "‼ x" := (map (cll_una cll_bang) x) (at level 60).
-Notation "⁇ x" := (map (cll_una cll_qmrk) x) (at level 60).
+  (* Modalities iterated over lists *)
 
-(* The empty list *)
+  Notation "‼ x" := (map (cll_una cll_bang) x) (at level 60).
+  Notation "⁇ x" := (map (cll_una cll_qmrk) x) (at level 60).
+
+End CLL_notations.
 
-Notation "∅" := nil.
+Import CLL_notations.
+
+(* The empty list *)
 
-Local Reserved Notation "Γ ⊢ Δ" (at level 70, no associativity).
+#[local] Notation "∅" := nil.
+#[local] Reserved Notation "Γ ⊢ Δ" (at level 70, no associativity).
 
 Section S_cll_restr_without_cut.
 

theories/ILL/EILL.v

@@ -13,6 +13,8 @@ From Stdlib Require Import List Permutation.
 
 From Undecidability.ILL Require Import ILL.
 
+Import ILL_notations.
+
 Set Implicit Arguments.
 
 Local Infix "~p" := (@Permutation _) (at level 70).

theories/ILL/ILL.v

@@ -35,24 +35,30 @@ Inductive ill_form : Set :=
 
 (* Symbols for cut&paste ⟙   ⟘   𝝐  ﹠ ⊗  ⊕  ⊸  !   ‼  ∅  ⊢ *)
 
-Notation "⟙" := (ill_cst ill_top).
-Notation "⟘" := (ill_cst ill_bot).
-Notation "𝟙" := (ill_cst ill_1).
+Module ILL_notations.
 
-Infix "&" := (ill_bin ill_with) (at level 50).
-Infix "⊗" := (ill_bin ill_times) (at level 50).
-Infix "⊕" := (ill_bin ill_plus) (at level 50).
-Infix "⊸" := (ill_bin ill_limp) (at level 51, right associativity).
+  Notation "⟙" := (ill_cst ill_top).
+  Notation "⟘" := (ill_cst ill_bot).
+  Notation "𝟙" := (ill_cst ill_1).
 
-Notation "'!' x" := (ill_ban x) (at level 52).
+  Infix "&" := (ill_bin ill_with) (at level 50).
+  Infix "⊗" := (ill_bin ill_times) (at level 50).
+  Infix "⊕" := (ill_bin ill_plus) (at level 50).
+  Infix "⊸" := (ill_bin ill_limp) (at level 51, right associativity).
 
-Notation "£" := ill_var.
+  Notation "'!' x" := (ill_ban x) (at level 52).
 
-Notation "‼ x" := (map ill_ban x) (at level 60).
+  Notation "£" := ill_var.
 
-Notation "∅" := nil (only parsing).
+  Notation "‼ x" := (map ill_ban x) (at level 60).
 
-Reserved Notation "l '⊢' x" (at level 70, no associativity).
+  Notation "∅" := nil (only parsing).
+
+End ILL_notations.
+
+Import ILL_notations.
+
+#[local] Reserved Notation "l '⊢' x" (at level 70, no associativity).
 
 Section S_ill_restr_without_cut.
 

theories/ILL/IMSELL.v

@@ -17,9 +17,9 @@ Set Implicit Arguments.
 
 Local Infix "~p" := (@Permutation _) (at level 70).
 
-Reserved Notation "A ⊸ B" (at level 51, right associativity, format "A ⊸ B").
-Reserved Notation "'![' m ']' x" (at level 52, format "![ m ] x").
-Reserved Notation "‼ x" (at level 60, format "‼ x").
+#[local] Reserved Notation "A ⊸ B" (at level 51, right associativity, format "A ⊸ B").
+#[local] Reserved Notation "'![' m ']' x" (at level 52, format "![ m ] x").
+#[local] Reserved Notation "‼ x" (at level 60, format "‼ x").
 
 Section IMSELL.
 
@@ -85,10 +85,21 @@ Section IMSELL.
 
 End IMSELL.
 
-Infix "⊸" := imsell_imp.
-Notation "![ m ] x" := (imsell_ban m x).
-Notation "£" := imsell_var.
-Notation "‼ Γ" := (imsell_lban Γ).
+Arguments imsell_var {_ _}.
+Arguments imsell_imp {_ _}.
+Arguments imsell_ban {_ _}.
+Arguments imsell_lban {_ _}.
+
+Module IMSELL_notations.
+
+  Infix "⊸" := imsell_imp.
+  Notation "![ m ] x" := (imsell_ban m x).
+  Notation "£" := imsell_var.
+  Notation "‼ Γ" := (imsell_lban Γ).
+
+End IMSELL_notations.
+
+Import IMSELL_notations.
 
 (* An IMSELL signature is a type of modalities pre-ordered
     and an upper-closed subset of exponentials *)

theories/ILL/Ll/eill.v

@@ -14,15 +14,14 @@ From Undecidability.Shared.Libs.DLW
 
 From Undecidability.ILL Require Import ILL EILL ill.
 
-Set Implicit Arguments.
+Import ILL_notations.
 
-Local Infix "~p" := (@Permutation _) (at level 70).
+Set Implicit Arguments.
 
 (* Symbols for cut&paste ⟙   ⟘   𝝐  ﹠ ⊗  ⊕  ⊸  ❗   ‼  ∅  ⊢ ⟦ ⟧ Γ Δ Σ *)
 
-Notation "⦑ c ⦒" := (eill_cmd_map c) (at level 0).
-
-Notation "Σ ; Γ ⊦ u" := (G_eill Σ Γ u) (at level 70, no associativity).
+#[local] Notation "⦑ c ⦒" := (eill_cmd_map c) (at level 0).
+#[local] Notation "Σ ; Γ ⊦ u" := (G_eill Σ Γ u) (at level 70, no associativity).
 
 Theorem g_eill_mono_Si Σ Σ' Γ u : incl Σ Σ' -> Σ; Γ ⊦ u -> Σ'; Γ ⊦ u.
 Proof.
@@ -47,7 +46,7 @@ Qed.
    the cut-free (!,&,-o) fragment
 *)
 
-Notation "Γ ⊢ A" := (S_ill_restr Γ A) (at level 70, no associativity).
+#[local] Notation "Γ ⊢ A" := (S_ill_restr Γ A) (at level 70, no associativity).
 
 Theorem G_eill_sound Σ Γ p : Σ; Γ ⊦ p -> map (fun c => !⦑c⦒) Σ ++ map £ Γ ⊢ £ p.
 Proof.

theories/ILL/Ll/eill_mm.v

@@ -18,9 +18,12 @@ From Undecidability.MinskyMachines.MM
 From Undecidability.ILL
   Require Import ILL EILL ill eill.
 
+Import ILL_notations.
+
 Set Implicit Arguments.
 
-Local Infix "~p" := (@Permutation _) (at level 70).
+#[local] Notation "⦑ c ⦒" := (eill_cmd_map c) (at level 0).
+#[local] Notation "Σ ; Γ ⊦ u" := (G_eill Σ Γ u) (at level 70, no associativity).
 
 (* ** MM reduces to eILL *)
 

theories/ILL/Ll/ill.v

@@ -15,6 +15,8 @@ From Undecidability.Shared.Libs.DLW
 From Undecidability.ILL
   Require Import ILL.
 
+Import ILL_notations.
+
 Set Implicit Arguments.
 
 Section obvious_links_between_fragments.

theories/ILL/Ll/ill_cll.v

@@ -127,8 +127,8 @@ Local Hint Resolve ill_cll_ill : core.
 Fact ill_cll_ill_list Γ : ⟪⟦Γ⟧⟫ = Γ.
 Proof. induction Γ; simpl; f_equal; auto. Qed.
 
-Fact ill_cll_lbang Γ : ⟦map ill_ban Γ⟧ = ‼⟦Γ⟧.
+Fact ill_cll_lbang Γ : ⟦map ill_ban Γ⟧ = map (cll_una cll_bang) ⟦Γ⟧.
 Proof. induction Γ; simpl; f_equal; auto. Qed.
 
-Fact cll_ill_lbang Γ : ⟪‼Γ⟫ = map ill_ban ⟪Γ⟫.
+Fact cll_ill_lbang Γ : ⟪map (cll_una cll_bang) Γ⟫ = map ill_ban ⟪Γ⟫.
 Proof. induction Γ; simpl; f_equal; auto. Qed.

theories/ILL/Ll/ill_cll_restr.v

@@ -37,6 +37,7 @@ Local Infix "~p" := (@Permutation _) (at level 70).
 
        derived from the work of H. Schellinx JLC 91 *)
 
+#[local] Notation "∅" := nil.
 
 Section S_ill_cll_restr.
 

theories/ILL/Ll/imsell.v

@@ -12,25 +12,24 @@ From Stdlib Require Import List Permutation.
 From Undecidability.ILL 
   Require Import IMSELL.
 
+Import IMSELL_notations.
+
 From Undecidability.Shared.Libs.DLW 
   Require Import utils pos vec.
 
 Set Implicit Arguments.
 
 (* * Intuionistic Multiplicative Linear Logic with several exponentials and modabilities *)
 
-Local Infix "~p" := (@Permutation _) (at level 70).
+(* 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 0, format "⟦ A ⟧").
-
 Section IMSELL.
 
   Variable bang : Type.
 
-  Notation "£" := (@imsell_var _ _).
-  Notation "‼ l" := (@imsell_lban nat bang l).
+  Implicit Type (Σ : list (bang * imsell_form nat bang)). 
 
   Fact imsell_lban_perm Σ Γ : Σ ~p Γ -> ‼Σ ~p ‼Γ.
   Proof. apply Permutation_map. Qed.
@@ -102,6 +101,8 @@ Section IMSELL.
 
 *)
 
+  Reserved Notation "'⟦' A '⟧'" (at level 0, format "⟦ A ⟧").
+
   Section Trivial_Phase_semantics.
 
     (* We only consider the monoids nat^n *)

theories/ILL/Ll/schellinx.v

@@ -14,6 +14,8 @@ From Undecidability.Shared.Libs.DLW
 
 From Undecidability.ILL Require Import ILL CLL ill_cll.
 
+Import CLL_notations.
+
 Set Implicit Arguments.
 
 (* Small inversion lemma *)
@@ -40,13 +42,13 @@ Tactic Notation "app" "inv" "nil" "in" hyp(H) :=
 
        derived from the work of H. Schellinx JLC 91 *)
 
-Local Infix "~p" := (@Permutation _) (at level 70).
-
 (* Γ ⊢i A stands for the sequent Γ ⊢ A is cut-free ILL provable *)
 (* Γ ⊢c Δ stands for the sequent Γ ⊢ Δ is cut-free CLL provable *)
 
-Notation "Γ '⊢i' A" := (S_ill Γ A) (at level 70, no associativity).
-Notation "Γ '⊢c' Δ" := (S_cll Γ Δ) (at level 70, no associativity).
+#[local] Notation "Γ '⊢i' A" := (S_ill Γ A) (at level 70, no associativity).
+#[local] Notation "Γ '⊢c' Δ" := (S_cll Γ Δ) (at level 70, no associativity).
+
+#[local] Notation "∅" := nil.
 
 Section ill_cll_is_sound.
 

theories/ILL/Reductions/EILL_CLL.v

@@ -19,7 +19,7 @@ Theorem EILL_CLL_cf_PROVABILITY : EILL_PROVABILITY ⪯ CLL_cf_PROVABILITY.
 Proof.
   apply reduces_dependent; exists.
   intros ((Σ,Γ),u).
-  exists ( map (fun c => cll_una cll_bang [⦑c⦒]) Σ 
+  exists ( map (fun c => cll_una cll_bang [eill_cmd_map c]) Σ 
         ++ map cll_var Γ, cll_var u::nil).
   apply G_eill_S_cll.
 Qed.

theories/ILL/Reductions/EILL_ILL.v

@@ -13,7 +13,11 @@ Require Import Undecidability.Synthetic.Definitions.
 Require Import Undecidability.Synthetic.ReducibilityFacts.
 
 From Undecidability.ILL
-  Require Import EILL ILL ill eill. 
+  Require Import EILL ILL ill eill.
+
+Import ILL_notations.
+
+#[local] Notation "⦑ c ⦒" := (eill_cmd_map c) (at level 0).
 
 Theorem EILL_rILL_cf_PROVABILITY : EILL_PROVABILITY ⪯ rILL_cf_PROVABILITY.
 Proof.

theories/ILL/Reductions/ndMM2_IMSELL.v

@@ -12,9 +12,11 @@ From Stdlib Require Import List Permutation Arith Lia.
 From Undecidability.MinskyMachines
   Require Import ndMM2.
 
-From Undecidability.ILL 
+From Undecidability.ILL
   Require Import IMSELL imsell.
 
+Import IMSELL_notations.
+
 From Undecidability.Shared.Libs.DLW 
   Require Import utils pos vec.
 
@@ -23,7 +25,6 @@ From Undecidability.Synthetic
 
 Set Implicit Arguments.
 
-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).
 
@@ -58,16 +59,14 @@ Section ndmm2_imsell.
   Hypothesis (Hai : a ≤ ∞) (Hbi : b ≤ ∞) (Hab : a ≰ b) (Hba : b ≰ a)
              (Ha : ~ U a) (Hb : ~ U b) (Hi : U ∞).
 
-  Implicit Type u v w : sig.
+  Implicit Type (u v w : sig) (l : list (sig * imsell_form nat sig)).
 
   Local Definition bang_le_refl : forall u, u ≤ u := IMSELL_refl _.
   Local Definition bang_le_trans : forall u v w, u ≤ v -> v ≤ w -> u ≤ w := IMSELL_trans _.
   Local Definition bang_U_clos : forall u v, U u -> u ≤ v -> U v := IMSELL_clos _.
 
   Hint Resolve Hai Hbi Ha Hb Hi Hab Hba bang_le_refl bang_U_clos : core.
 
-  Notation "£" := (@imsell_var _ _).
-  Notation "‼ l" := (@imsell_lban nat sig l).
   Notation "‼∞" := (map (fun A => ![∞]A)).
 
   Local Definition formA : imsell_form nat sig := ![a](£0).
@@ -370,7 +369,7 @@ Proof.
   intros (a & b & i & ?).
   apply reduces_dependent; exists.
   intros (Σ & u & x & y).
-  exists (ndmm2_imsell_ctx _ a b i Σ x y, imsell_var _ (2+u)).
+  exists (ndmm2_imsell_ctx _ a b i Σ x y, imsell_var (2+u)).
   apply ndmm2_imsell_correct; simpl; tauto.
 Qed.
 

theories/SOL/Util/PA2_facts.v

@@ -7,7 +7,7 @@ From Undecidability.SOL.Util Require Import Syntax Subst Tarski.
 From Undecidability.Synthetic Require Import Definitions DecidabilityFacts EnumerabilityFacts ListEnumerabilityFacts ReducibilityFacts.
 Require Import Undecidability.Shared.Dec.
 
-Import VectorNotations SubstNotations SOLNotations PA2Notations.
+Import VectorNotations SubstNotations SOLNotations.
 
 Arguments Vector.cons {_} _ {_} _, _ _ _ _.