diff --git a/theories/ILL/CLL.v b/theories/ILL/CLL.v
index a6ad464f..319acc1a 100644
--- a/theories/ILL/CLL.v
+++ b/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.
 
diff --git a/theories/ILL/EILL.v b/theories/ILL/EILL.v
index a56b74c3..501f5072 100644
--- a/theories/ILL/EILL.v
+++ b/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).
diff --git a/theories/ILL/ILL.v b/theories/ILL/ILL.v
index 3df8cfee..10bcf64f 100644
--- a/theories/ILL/ILL.v
+++ b/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.
 
diff --git a/theories/ILL/IMSELL.v b/theories/ILL/IMSELL.v
index caa8ef09..8778cdfb 100644
--- a/theories/ILL/IMSELL.v
+++ b/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 *)
diff --git a/theories/ILL/Ll/eill.v b/theories/ILL/Ll/eill.v
index 5e8e49f8..af82cee4 100644
--- a/theories/ILL/Ll/eill.v
+++ b/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.
diff --git a/theories/ILL/Ll/eill_mm.v b/theories/ILL/Ll/eill_mm.v
index e982cf7d..3790355d 100644
--- a/theories/ILL/Ll/eill_mm.v
+++ b/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 *)
 
diff --git a/theories/ILL/Ll/ill.v b/theories/ILL/Ll/ill.v
index b273e656..10d6bdd2 100644
--- a/theories/ILL/Ll/ill.v
+++ b/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.
diff --git a/theories/ILL/Ll/ill_cll.v b/theories/ILL/Ll/ill_cll.v
index 2eced547..8a09f8a5 100644
--- a/theories/ILL/Ll/ill_cll.v
+++ b/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.
diff --git a/theories/ILL/Ll/ill_cll_restr.v b/theories/ILL/Ll/ill_cll_restr.v
index d38c1bd8..68e80cbf 100644
--- a/theories/ILL/Ll/ill_cll_restr.v
+++ b/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.
 
diff --git a/theories/ILL/Ll/imsell.v b/theories/ILL/Ll/imsell.v
index 6b5bdb3e..04a9bfb4 100644
--- a/theories/ILL/Ll/imsell.v
+++ b/theories/ILL/Ll/imsell.v
@@ -12,6 +12,8 @@ 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.
 
@@ -19,18 +21,15 @@ 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 *)
diff --git a/theories/ILL/Ll/schellinx.v b/theories/ILL/Ll/schellinx.v
index a4176d1e..56b43e1b 100644
--- a/theories/ILL/Ll/schellinx.v
+++ b/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.
 
diff --git a/theories/ILL/Reductions/EILL_CLL.v b/theories/ILL/Reductions/EILL_CLL.v
index 39ed834a..f65b169c 100644
--- a/theories/ILL/Reductions/EILL_CLL.v
+++ b/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.
diff --git a/theories/ILL/Reductions/EILL_ILL.v b/theories/ILL/Reductions/EILL_ILL.v
index 841f0f71..d7c1a1f6 100644
--- a/theories/ILL/Reductions/EILL_ILL.v
+++ b/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.
diff --git a/theories/ILL/Reductions/ndMM2_IMSELL.v b/theories/ILL/Reductions/ndMM2_IMSELL.v
index 7cc4a78d..e49b5e31 100644
--- a/theories/ILL/Reductions/ndMM2_IMSELL.v
+++ b/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,7 +59,7 @@ 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 _.
@@ -66,8 +67,6 @@ Section ndmm2_imsell.
 
   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.
 
diff --git a/theories/SOL/Util/PA2_facts.v b/theories/SOL/Util/PA2_facts.v
index eea434d5..f29887df 100644
--- a/theories/SOL/Util/PA2_facts.v
+++ b/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 {_} _ {_} _, _ _ _ _.
 
diff --git a/theories/TM/Reductions/HaltTM_1_to_SBTM_HALT.v b/theories/TM/Reductions/HaltTM_1_to_SBTM_HALT.v
index e85dfe5e..dd58281b 100644
--- a/theories/TM/Reductions/HaltTM_1_to_SBTM_HALT.v
+++ b/theories/TM/Reductions/HaltTM_1_to_SBTM_HALT.v
@@ -8,7 +8,8 @@ From Stdlib Require Import PeanoNat Lia.
 #[local] Unset Strict Implicit.
 
 From Stdlib Require Import List ssreflect ssrbool ssrfun.
-Import ListNotations SBTMNotations.
+Import Vector.VectorNotations SBTMNotations ListNotations.
+Open Scope list.
 
 Set Default Goal Selector "!".
 
@@ -159,9 +160,8 @@ Section Construction.
   Lemma decode_encode_space (x : space) : decode_space (encode_space x) = x.
   Proof. by apply: ListFin.decode_encode. Qed.
 
-  #[local] Notation "| a |" := (Vector.cons _ a 0 (Vector.nil _)).
-
   #[local] Notation encode_state q := (encode_space (space_base q)).
+  Open Scope vector.
 
   Definition go_back (d : direction) :=
     match d with
@@ -212,7 +212,7 @@ Section Construction.
             | true => Some (encode_space (space_read q_base), true, go_left)
             (* case a = false, no symbol *)
             | false => 
-              match TM.trans M (q_base, | None |) with
+              match TM.trans M (q_base, [ None ]) with
               | (q_next, result) =>
                   match Vector.hd result with
                   (* case write b, move *)
@@ -227,7 +227,7 @@ Section Construction.
         end).
     + (* case space_read *)
       refine ( 
-        match TM.trans M (q_read, | Some a |) with
+        match TM.trans M (q_read, [ Some a ]) with
         | (q_next, result) =>
           match Vector.hd result with
           (* case write bL, Lmove *)
@@ -260,7 +260,7 @@ Section Construction.
   Lemma simulation_step q t : TM.halt M q = false ->
     exists k,
       (omap (fun '(q', t') => (q', truncate_tape t')) (steps (S k) (encode_state q, encode_tape t))) =
-        Some (encode_config (TM_step (TM_facts.mk_mconfig q (| t |)))).
+        Some (encode_config (TM_step (TM_facts.mk_mconfig q ([ t ])))).
   Proof.
     move=> Hq. case: t.
     - (* case niltape *)
diff --git a/theories/TM/Reductions/SBTM_HALT_to_HaltTM_1.v b/theories/TM/Reductions/SBTM_HALT_to_HaltTM_1.v
index 292649c1..7c91efd9 100644
--- a/theories/TM/Reductions/SBTM_HALT_to_HaltTM_1.v
+++ b/theories/TM/Reductions/SBTM_HALT_to_HaltTM_1.v
@@ -8,12 +8,10 @@ From Stdlib Require Import PeanoNat Lia.
 #[local] Unset Strict Implicit.
 
 From Stdlib Require Import List ssreflect ssrbool ssrfun.
-Import ListNotations SBTMNotations.
+Import ListNotations SBTMNotations Vector.VectorNotations.
 
 Set Default Goal Selector "!".
 
-#[local] Notation "| a |" := (Vector.cons _ a 0 (Vector.nil _)).
-
 Section Construction.
   (* input SBTM and initial state *)
   Context (M : SBTM) (q0 : state M).
@@ -48,12 +46,12 @@ Section Construction.
     refine (
       match q with
       | Some qM => _
-      | None => (None, | (None, TM.Nmove) | )
+      | None => (None, [ (None, TM.Nmove) ] )
       end).
     refine (
       match trans' M (qM, get_symbol (Vector.hd bs)) with
-      | None => (None, | (None, TM.Nmove) | )
-      | Some (q', a', d') => (Some q', | (Some a',encode_direction d') | )
+      | None => (None, [ (None, TM.Nmove) ] )
+      | Some (q', a', d') => (Some q', [ (Some a',encode_direction d') ] )
       end).
   Defined.
 
@@ -61,7 +59,7 @@ Section Construction.
   #[local] Notation TM_config := (@TM_facts.mconfig (finType_CS bool) (TM.state M') 1).
 
   Definition encode_config : config M -> TM_config :=
-    fun '(q, t) => TM_facts.mk_mconfig (Some q) (| encode_tape t |).
+    fun '(q, t) => TM_facts.mk_mconfig (Some q) ([ encode_tape t ]).
 
   Definition canonize_tape (t : TM.tape (finType_CS bool)) :=
     match t with
@@ -89,8 +87,8 @@ Section Construction.
 
   Lemma TM_step_canonize_tape oq oq1 t1 t'1 oq2 t2 t'2 :
     canonize_tape t1 = canonize_tape t2 ->
-    TM_step (TM_facts.mk_mconfig oq (| t1 |)) = TM_facts.mk_mconfig oq1 (| t'1 |) ->
-    TM_step (TM_facts.mk_mconfig oq (| t2 |)) = TM_facts.mk_mconfig oq2 (| t'2 |) ->
+    TM_step (TM_facts.mk_mconfig oq ([ t1 ])) = TM_facts.mk_mconfig oq1 ([ t'1 ]) ->
+    TM_step (TM_facts.mk_mconfig oq ([ t2 ])) = TM_facts.mk_mconfig oq2 ([ t'2 ]) ->
     oq1 = oq2 /\ canonize_tape t'1 = canonize_tape t'2.
   Proof.
     move=> Ht1t2.
@@ -105,8 +103,8 @@ Section Construction.
 
   Lemma TM_loopM_canonize_tape (oq : TM.state M') t1 t2 k q' t'1 :
     canonize_tape t1 = canonize_tape t2 ->
-    TM_facts.loopM (TM_facts.mk_mconfig oq (| t1 |)) k = Some (TM_facts.mk_mconfig q' t'1) ->
-    { t'2 | TM_facts.loopM (TM_facts.mk_mconfig oq (| t2 |)) k = Some (TM_facts.mk_mconfig q' t'2) }.
+    TM_facts.loopM (TM_facts.mk_mconfig oq ([ t1 ])) k = Some (TM_facts.mk_mconfig q' t'1) ->
+    { t'2 | TM_facts.loopM (TM_facts.mk_mconfig oq ([ t2 ])) k = Some (TM_facts.mk_mconfig q' t'2) }.
   Proof.
     elim: k oq t1 t2.
     { move=> > _ /=. case: (halt' _) => [|]; last done.
@@ -124,7 +122,7 @@ Section Construction.
   (* step simulation up to canonize_tape *)
   Lemma simulation_step q t q' t' : step M (q, t) = Some (q', t') ->
     { t'' |
-      TM_step (encode_config (q, t)) = TM_facts.mk_mconfig (Some q') (| t'' |) /\
+      TM_step (encode_config (q, t)) = TM_facts.mk_mconfig (Some q') ([ t'' ]) /\
       encode_tape t' = canonize_tape t'' }.
   Proof.
     rewrite /step /TM_facts.step /=.
@@ -135,7 +133,7 @@ Section Construction.
   Qed.
 
   Lemma simulation_halt q t : step M (q, t) = None ->
-    TM_step (encode_config (q, t)) = TM_facts.mk_mconfig None (| encode_tape t |).
+    TM_step (encode_config (q, t)) = TM_facts.mk_mconfig None ([ encode_tape t ]).
   Proof.
     rewrite /step /TM_facts.step /=.
     move: t => [[ls a] rs] /=.
@@ -144,7 +142,7 @@ Section Construction.
 
   Lemma simulation q t k :
     steps M k (q, t) = None ->
-    exists q' ts', TM.eval M' (Some q) (| encode_tape t |) q' ts'.
+    exists q' ts', TM.eval M' (Some q) ([ encode_tape t ]) q' ts'.
   Proof.
     elim: k q t; first done.
     move=> k IH q t.
@@ -155,7 +153,7 @@ Section Construction.
       move=> /(_ ltac:(by case: (t''))). move=> [{}t''' ?].
       exists q''', t'''. apply /TM_facts.TM_eval_iff. exists (S k').
       by rewrite /= HM'.
-    - move=> _. exists None, (| encode_tape t |).
+    - move=> _. exists None, ([ encode_tape t ]).
       apply /TM_facts.TM_eval_iff. exists 1.
       move: E.
       rewrite /= /step /TM_facts.step /=.
@@ -164,7 +162,7 @@ Section Construction.
   Qed.
 
   Lemma inverse_simulation q t q' ts' :
-    TM.eval M' (Some q) (| encode_tape t |) q' ts' ->
+    TM.eval M' (Some q) ([ encode_tape t ]) q' ts' ->
     exists k, steps M k (q, t) = None.
   Proof.
     move=> /TM_facts.TM_eval_iff => - [k Hk]. exists k.
@@ -186,7 +184,7 @@ Theorem reduction :
   SBTM_HALT ⪯ TM.HaltTM 1.
 Proof.
   exists ((fun '(existT _ M (q, t)) =>
-    existT2 _ _ (finType_CS bool) (M' M q) (| encode_tape t |)) ).
+    existT2 _ _ (finType_CS bool) (M' M q) ([ encode_tape t ])) ).
   move=> [M [q t]] /=. split.
   - by move=> [k] /simulation => /(_ q).
   - by move=> [?] [?] /inverse_simulation.
diff --git a/theories/_CoqProject b/theories/_CoqProject
index 7f7b65c7..3f1653a9 100644
--- a/theories/_CoqProject
+++ b/theories/_CoqProject
@@ -1,6 +1,6 @@
 -Q . Undecidability
 
--arg -w -arg -notation-overridden,-stdlib-vector# ,-notation-incompatible-prefix,-closed-notation-not-level-0,-postfix-notation-not-level-1
+-arg -w -arg -stdlib-vector,-notation-overridden #,-notation-incompatible-prefix,-closed-notation-not-level-0,-postfix-notation-not-level-1
 -arg "-set" -arg "'Default Proof Using = Type'"
 COQDOCFLAGS = "--charset utf-8 -s --with-header ../website/resources/header.html --with-footer ../website/resources/footer.html --index indexpage"