From f6cd80d699741a0725deaacfcc4df5eb1de432cf Mon Sep 17 00:00:00 2001
From: skylee03 <i@skylee.xyz>
Date: Thu, 6 Aug 2026 20:29:21 +0800
Subject: [PATCH 01/24] fix deprecated-from-Coq

---
 theories/Autosubst_Basics.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/theories/Autosubst_Basics.v b/theories/Autosubst_Basics.v
index d1dea83..6582259 100644
--- a/theories/Autosubst_Basics.v
+++ b/theories/Autosubst_Basics.v
@@ -4,8 +4,8 @@
   substitutions.
 *)
 
-From Coq.Program Require Import Tactics.
-From Coq Require Import PeanoNat List FunctionalExtensionality.
+From Stdlib.Program Require Import Tactics.
+From Stdlib Require Import PeanoNat List FunctionalExtensionality.
 
 (** Annotate "a" with additional information. *)
 Definition annot {A B} (a : A) (b : B) : A := a.

From a4fda88911b3dc1991bcf903d4ef9cfac8189029 Mon Sep 17 00:00:00 2001
From: skylee03 <i@skylee.xyz>
Date: Thu, 6 Aug 2026 20:34:09 +0800
Subject: [PATCH 02/24] fix deprecated-missing-stdlib

---
 examples/plain/Context.v           | 2 +-
 examples/plain/Decidable.v         | 2 +-
 examples/plain/POPLmark.v          | 2 +-
 examples/plain/Size.v              | 2 +-
 theories/Autosubst_MMapInstances.v | 2 +-
 5 files changed, 5 insertions(+), 5 deletions(-)

diff --git a/examples/plain/Context.v b/examples/plain/Context.v
index e8f77d0..896c3fa 100644
--- a/examples/plain/Context.v
+++ b/examples/plain/Context.v
@@ -1,5 +1,5 @@
 (** * Context *)
-Require Import Lia ZArith List Program.Equality.
+From Stdlib Require Import Lia ZArith List Program.Equality.
 Require Import Autosubst.Autosubst.
 
 Fixpoint atn {X} l n (x : X) :=
diff --git a/examples/plain/Decidable.v b/examples/plain/Decidable.v
index ef0c966..90b696b 100644
--- a/examples/plain/Decidable.v
+++ b/examples/plain/Decidable.v
@@ -1,5 +1,5 @@
 (** * Notation for decidable propositions *)
-Require Import Arith.
+From Stdlib Require Import Arith.
 
 Definition dec (X : Prop) : Type := {X} + {~ X}.
 Class Dec (X : Prop) : Type := decide : dec X.
diff --git a/examples/plain/POPLmark.v b/examples/plain/POPLmark.v
index f35113b..c49b212 100644
--- a/examples/plain/POPLmark.v
+++ b/examples/plain/POPLmark.v
@@ -5,7 +5,7 @@
     formalization of syntactic theories.  We solve part 1, that is,
     progress and preservation of System F with subtyping.  *)
 
-Require Import Program.Equality List Lia.
+From Stslib Require Import Program.Equality List Lia.
 Require Import Autosubst.Autosubst.
 Require Import Size Decidable Context.
 
diff --git a/examples/plain/Size.v b/examples/plain/Size.v
index 0a8669b..ba335b2 100644
--- a/examples/plain/Size.v
+++ b/examples/plain/Size.v
@@ -1,5 +1,5 @@
 (** * Support for Size Induction *)
-Require Import ZArith Lia List Program.Equality.
+From Stdlib Require Import ZArith Lia List Program.Equality.
 Require Import Autosubst.Autosubst_Basics.
 
 Class Size (A : Type) := size : A -> nat.
diff --git a/theories/Autosubst_MMapInstances.v b/theories/Autosubst_MMapInstances.v
index 5ad7dba..2cb9c8d 100644
--- a/theories/Autosubst_MMapInstances.v
+++ b/theories/Autosubst_MMapInstances.v
@@ -4,7 +4,7 @@
 *)
 Require Import Autosubst_Basics Autosubst_MMap.
 
-Require List.
+From Stdlib Require List.
 
 Section MMapInstances.
 

From cbe84e12acbec2b14f6b1b9351ac454b5f1f65bf Mon Sep 17 00:00:00 2001
From: skylee03 <i@skylee.xyz>
Date: Thu, 6 Aug 2026 20:36:55 +0800
Subject: [PATCH 03/24] fix notation-for-abbreviation

---
 examples/plain/POPLmark.v    | 2 +-
 theories/Autosubst_Classes.v | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/examples/plain/POPLmark.v b/examples/plain/POPLmark.v
index c49b212..3ba96e0 100644
--- a/examples/plain/POPLmark.v
+++ b/examples/plain/POPLmark.v
@@ -5,7 +5,7 @@
     formalization of syntactic theories.  We solve part 1, that is,
     progress and preservation of System F with subtyping.  *)
 
-From Stslib Require Import Program.Equality List Lia.
+From Stdlib Require Import Program.Equality List Lia.
 Require Import Autosubst.Autosubst.
 Require Import Size Decidable Context.
 
diff --git a/theories/Autosubst_Classes.v b/theories/Autosubst_Classes.v
index b3f608c..279b199 100644
--- a/theories/Autosubst_Classes.v
+++ b/theories/Autosubst_Classes.v
@@ -114,7 +114,7 @@ Definition up {T} `{Ids T} `{Rename T} (sigma : var -> T) : var -> T :=
   ids 0 .: sigma >>> rename (+1).
 Arguments up {T _ _} sigma x : simpl never.
 
-Notation upn := (iterate up).
+Abbreviation upn := (iterate up).
 
 Definition upren (xi : var -> var) : (var -> var) := 0 .: xi >>> S.
 

From b3e5e61b84c4d35463dbd11eb5f5cc515a46501b Mon Sep 17 00:00:00 2001
From: skylee03 <i@skylee.xyz>
Date: Thu, 6 Aug 2026 21:04:54 +0800
Subject: [PATCH 04/24] fix deprecated-end-tac

---
 examples/ssr/CR.v            | 26 ++++++-------
 examples/ssr/POPLmark.v      | 72 ++++++++++++++++++------------------
 examples/ssr/SystemF_SN.v    | 32 ++++++++--------
 examples/ssr/pred_CC_omega.v | 24 ++++++------
 4 files changed, 77 insertions(+), 77 deletions(-)

diff --git a/examples/ssr/CR.v b/examples/ssr/CR.v
index d6cbd27..25b5f63 100644
--- a/examples/ssr/CR.v
+++ b/examples/ssr/CR.v
@@ -94,16 +94,16 @@ Lemma step_pstep s t : step s t -> pstep s t.
 Proof. elim; eauto using pstep. Qed.
 
 Lemma pstep_red s t : pstep s t -> red s t.
-Proof with eauto with red_congr.
-  elim=> {s t} //=... move=> s1 s2 t1 t2 _ A _ B.
-  apply: (star_trans (App (Lam s2) t2))... exact/star1/step_beta.
+Proof.
+  elim=> {s t} //=; eauto with red_congr. move=> s1 s2 t1 t2 _ A _ B.
+  apply: (star_trans (App (Lam s2) t2)); eauto with red_congr. exact/star1/step_beta.
 Qed.
 
 Lemma pstep_subst sigma s t :
   pstep s t -> pstep s.[sigma] t.[sigma].
-Proof with eauto using pstep.
-  move=> A. elim: A sigma => /=... move=> s1 s2 t1 t2 _ A _ B sigma.
-  eapply pstep_ebeta... by autosubst.
+Proof.
+  move=> A. elim: A sigma => /=; eauto using pstep. move=> s1 s2 t1 t2 _ A _ B sigma.
+  eapply pstep_ebeta; eauto using pstep. by autosubst.
 Qed.
 
 Lemma psstep_up sigma tau :
@@ -114,10 +114,10 @@ Qed.
 
 Lemma pstep_compat sigma tau s t :
   psstep sigma tau -> pstep s t -> pstep s.[sigma] t.[tau].
-Proof with eauto using pstep, psstep_up.
-  move=> A B. elim: B sigma tau A; asimpl...
+Proof.
+  move=> A B. elim: B sigma tau A; asimpl; eauto using pstep, psstep_up.
   move=> s1 s2 t1 t2 _ A _ B sigma tau C.
-  apply: (@pstep_ebeta _ (s2.[up tau]) _ (t2.[tau])); asimpl...
+  apply: (@pstep_ebeta _ (s2.[up tau]) _ (t2.[tau])); asimpl; eauto using pstep, psstep_up.
 Qed.
 
 Lemma pstep_compat_beta s1 s2 t1 t2 :
@@ -127,11 +127,11 @@ Proof.
 Qed.
 
 Lemma rho_triangle : triangle pstep rho.
-Proof with eauto using pstep.
-  move=> s t. elim=> {s t} //=...
+Proof.
+  move=> s t. elim=> {s t} //=; eauto using pstep.
   - move=> s1 s2 t1 t2 _ A _ B. exact: pstep_compat_beta.
-  - move=> s1 s2 t1 t2 A ih1 _ ih2. case: s1 A ih1 => //=...
-    move=> s A ih1. inv A. inv ih1...
+  - move=> s1 s2 t1 t2 A ih1 _ ih2. case: s1 A ih1 => //=; eauto using pstep.
+    move=> s A ih1. inv A. inv ih1; eauto using pstep.
 Qed.
 
 Theorem church_rosser :
diff --git a/examples/ssr/POPLmark.v b/examples/ssr/POPLmark.v
index e716fca..a564546 100644
--- a/examples/ssr/POPLmark.v
+++ b/examples/ssr/POPLmark.v
@@ -105,13 +105,13 @@ Lemma sub_narrow_t Gamma Delta A B :
   (forall x, x < size Gamma ->
     Delta`_x = Gamma`_x \/ transitivity_at (Gamma`_x)) ->
   SUB Gamma |- A <: B -> SUB Delta |- A <: B.
-Proof with eauto using sub.
-  move=> h1 h2 h3 ty. elim: ty Delta h1 h2 h3 => {Gamma A B} /=...
-  - move=> Gamma x A lt _ ih Delta h1 h2 h3. apply: sub_var_trans...
-    case: (h3 x lt) => [->|]...
-  - move=> Gamma A1 A2 B1 B2 _ ih1 _ ih2 Delta h1 h2 h3. apply: sub_all...
-    apply: ih2 => [[|x /h1]|[|x /h2/sub_weak]|[_|x /h3[|]]] //=...
-    move=>->... move=> tr. right. exact: transitivity_ren.
+Proof.
+  move=> h1 h2 h3 ty. elim: ty Delta h1 h2 h3 => {Gamma A B} /=; eauto using sub.
+  - move=> Gamma x A lt _ ih Delta h1 h2 h3. apply: sub_var_trans; eauto using sub.
+    case: (h3 x lt) => [->|]; eauto using sub.
+  - move=> Gamma A1 A2 B1 B2 _ ih1 _ ih2 Delta h1 h2 h3. apply: sub_all; eauto using sub.
+    apply: ih2 => [[|x /h1]|[|x /h2/sub_weak]|[_|x /h3[|]]] //=; eauto using sub.
+    move=>->; eauto using sub. move=> tr. right. exact: transitivity_ren.
 Qed.
 
 Definition is_var (A : type) : bool := if A is TyVar _ then true else false.
@@ -120,20 +120,20 @@ Lemma sub_trans_snoc Gamma B C :
   (forall A, ~~is_var A ->
     SUB Gamma |- A <: B -> SUB Gamma |- B <: C -> SUB Gamma |- A <: C) ->
   forall A, SUB Gamma |- A <: B -> SUB Gamma |- B <: C -> SUB Gamma |- A <: C.
-Proof with eauto using sub.
-  move=> h A ty. elim: ty C h =>{Gamma A B}... move=> Gamma A C h1 h2. inv h2...
+Proof.
+  move=> h A ty. elim: ty C h =>{Gamma A B}; eauto using sub. move=> Gamma A C h1 h2. inv h2; eauto using sub.
 Qed.
 
 Lemma sub_trans_t B : transitivity_at B.
-Proof with eauto using sub.
-  elim: B => [x||B1 ih1 B2 ih2|B1 ih1 B2 ih2] Gamma A C xi; asimpl...
+Proof.
+  elim: B => [x||B1 ih1 B2 ih2|B1 ih1 B2 ih2] Gamma A C xi; asimpl; eauto using sub.
   - apply: sub_trans_snoc A => A e ty. by inv ty.
-  - move=> t1 t2. inv t2...
-  - apply: sub_trans_snoc A => A e ty1 ty2. inv ty1 => //. inv ty2...
-  - apply: sub_trans_snoc A => A e ty1 ty2. inv ty1 => //. inv ty2...
-    apply: sub_all... eapply ih2... move: H3. apply: sub_narrow_t...
+  - move=> t1 t2. inv t2; eauto using sub.
+  - apply: sub_trans_snoc A => A e ty1 ty2. inv ty1 => //. inv ty2; eauto using sub.
+  - apply: sub_trans_snoc A => A e ty1 ty2. inv ty1 => //. inv ty2; eauto using sub.
+    apply: sub_all; eauto using sub. eapply ih2; eauto using sub. move: H3. apply: sub_narrow_t; eauto using sub.
     + case=> //= _. exact: sub_weak.
-    + move=> [|x] _... right => /=. asimpl. exact: transitivity_ren.
+    + move=> [|x] _; eauto using sub. right => /=. asimpl. exact: transitivity_ren.
 Qed.
 
 Corollary sub_trans Gamma A B C :
@@ -152,10 +152,10 @@ Qed.
 Lemma sub_subst Gamma Delta A B sigma :
   (forall x, x < size Gamma -> SUB Delta |- sigma x <: (Gamma`_x).[sigma]) ->
   SUB Gamma |- A <: B -> SUB Delta |- A.[sigma] <: B.[sigma].
-Proof with eauto using sub.
-  move=> h ty. elim: ty Delta sigma h => {A B} Gamma...
+Proof.
+  move=> h ty. elim: ty Delta sigma h => {A B} Gamma; eauto using sub.
   - move=> x A lt _ ih Delta sigma h /=. apply: sub_trans (h _ lt) _. exact: ih.
-  - move=> A1 A2 B1 B2 _ ih1 _ ih2 Delta sigma h /=. apply: sub_all...
+  - move=> A1 A2 B1 B2 _ ih1 _ ih2 Delta sigma h /=. apply: sub_all; eauto using sub.
     apply: ih2 => -[_|x /h/sub_weak]. apply: sub_var_trans => //. autosubst.
     autosubst.
 Qed.
@@ -221,9 +221,9 @@ Lemma ty_ren Delta Gamma1 Gamma2 s A xi :
   (forall x, x < size Gamma1 -> xi x < size Gamma2) ->
   (forall x, x < size Gamma1 -> Gamma2``_(xi x) = Gamma1``_x) ->
   TY Delta;Gamma1 |- s : A -> TY Delta;Gamma2 |- s.[ren xi] : A.
-Proof with eauto using ty.
-  move=> h1 h2 ty. elim: ty Gamma2 xi h1 h2 => {Delta Gamma1 s A} /=...
-  - move=> Delta Gamma1 x lt Gamma2 xi h1 h2. rewrite -h2 //. apply: ty_var...
+Proof.
+  move=> h1 h2 ty. elim: ty Gamma2 xi h1 h2 => {Delta Gamma1 s A} /=; eauto using ty.
+  - move=> Delta Gamma1 x lt Gamma2 xi h1 h2. rewrite -h2 //. apply: ty_var; eauto using ty.
   - move=> Delta Gamma1 A B s _ ih Gamma2 xi h1 h2. asimpl. apply: ty_abs.
     by apply: ih => [[|x/h1]|[|x/h2]].
   - move=> Delta Gamma1 A B s _ ih Gamma2 xi h1 h2. apply: ty_tabs.
@@ -238,8 +238,8 @@ Proof. exact: ty_ren. Qed.
 Lemma ty_hsubst Delta1 Delta2 Gamma s A sigma :
   (forall x, x < size Delta1 -> SUB Delta2 |- sigma x <: (Delta1`_x).[sigma]) ->
   TY Delta1;Gamma |- s : A -> TY Delta2;Gamma..[sigma] |- s.|[sigma] :A.[sigma].
-Proof with eauto using ty.
-  move=> h ty. elim: ty Delta2 sigma h => {Delta1 Gamma s A}/=...
+Proof.
+  move=> h ty. elim: ty Delta2 sigma h => {Delta1 Gamma s A}/=; eauto using ty.
   - move=> Delta1 Gamma x lt Delta2 sigma h. apply: ty_evar. by rewrite get_map.
     by rewrite size_map.
   - move=> Delta1 Gamma A B s _ ih Delta2 sigma h. apply: ty_tabs.
@@ -260,10 +260,10 @@ Proof. apply: ty_hsubst => x /= lt. exact: sub_var_trans. Qed.
 Lemma ty_subst Delta Gamma1 Gamma2 s A sigma :
   (forall x, x < size Gamma1 -> TY Delta;Gamma2 |- sigma x : Gamma1``_x) ->
   TY Delta;Gamma1 |- s : A -> TY Delta;Gamma2 |- s.[sigma] : A.
-Proof with eauto using ty.
-  move=> h ty. elim: ty Gamma2 sigma h => {Delta Gamma1 s A}/=...
+Proof.
+  move=> h ty. elim: ty Gamma2 sigma h => {Delta Gamma1 s A}/=; eauto using ty.
   - move=> Delta Gamma1 A B s _ ih Gamma2 sigma h /=. apply: ty_abs.
-    apply: ih. move=> [_|x/h/ty_weak]... autosubst.
+    apply: ih. move=> [_|x/h/ty_weak]; eauto using ty. autosubst.
   - move=> Delta Gamma1 A B s _ ih Gamma2 sigma h. apply: ty_tabs. apply: ih.
     move=> x. rewrite size_map => lt. rewrite get_map //=. exact/ty_tweak/h.
 Qed.
@@ -334,11 +334,11 @@ Proof. move=> ty. exact: ty_inv_tabs' ty _. Qed.
 
 Theorem preservation Delta Gamma s t A :
   TY Delta;Gamma |- s : A -> EV s => t -> TY Delta;Gamma |- t : A.
-Proof with eauto using ty.
-  move=> ty. elim: ty t => {Delta Gamma s A}...
+Proof.
+  move=> ty. elim: ty t => {Delta Gamma s A}; eauto using ty.
   - move=> Delta Gamma x _ t ev. by inv ev.
   - move=> Delta Gamma A B s _ i t ev. by inv ev.
-  - move=> Delta Gamma A B s t ty1 ih1 ty2 ih2 u ev. inv ev...
+  - move=> Delta Gamma A B s t ty1 ih1 ty2 ih2 u ev. inv ev; eauto using ty.
     move: ty1 => /ty_inv_abs. exact: ty_beta.
   - move=> Delta Gamma A B s _ _ t ev. by inv ev.
   - move=> Delta Gamma A B C s ty ih sub t ev. inv ev.
@@ -381,16 +381,16 @@ Qed.
 
 Lemma ev_progress' Delta Gamma s A :
   TY Delta;Gamma |- s : A -> Gamma = [::] -> value s \/ exists t, EV s => t.
-Proof with eauto using eval.
+Proof.
   elim=> {Delta Gamma s A} /=; try solve [intuition].
   - move=> _ Gamma x lt eqn. by subst.
   - move=> Delta Gamma A B s t ty1 ih1 _ ih2 eqn. right.
-    case: (ih1 eqn) => {ih1} [vs|[s' h1]]...
-    case: (ih2 eqn) => {ih2 eqn} [vt|[t' h2]]...
-    case: s {ty1 vs} (canonical_arr _ _ _ _ _ ty1 vs) => //...
+    case: (ih1 eqn) => {ih1} [vs|[s' h1]]; eauto using eval.
+    case: (ih2 eqn) => {ih2 eqn} [vt|[t' h2]]; eauto using eval.
+    case: s {ty1 vs} (canonical_arr _ _ _ _ _ ty1 vs) => //; eauto using eval.
   - move=> Delta Gamma A B C s ty ih sub eqn. right.
-    case: (ih eqn) => {ih eqn}[vs|[s' h]]...
-    case: s {ty vs} (canonical_all _ _ _ _ _ ty vs) => //...
+    case: (ih eqn) => {ih eqn}[vs|[s' h]]; eauto using eval.
+    case: s {ty vs} (canonical_all _ _ _ _ _ ty vs) => //; eauto using eval.
 Qed.
 
 Theorem ev_progress s A:
diff --git a/examples/ssr/SystemF_SN.v b/examples/ssr/SystemF_SN.v
index 5c55abf..65d3b6b 100644
--- a/examples/ssr/SystemF_SN.v
+++ b/examples/ssr/SystemF_SN.v
@@ -209,22 +209,22 @@ Proof. by move=> H1 H2 [|i] //=. Qed.
 
 Lemma L_reducible T rho :
   admissible rho -> reducible (L T rho).
-Proof with eauto using step.
-  elim: T rho => /=[i|A ih1 B ih2|A ih] rho safe...
+Proof.
+  elim: T rho => /=[i|A ih1 B ih2|A ih] rho safe; eauto using step.
   - constructor.
-    + move=> s h. apply: (@sn_closed (TeVar 0)). apply: (p_sn (P := L B rho))...
+    + move=> s h. apply: (@sn_closed (TeVar 0)). apply: (p_sn (P := L B rho)); eauto using step.
       eapply h. eapply reducible_var; eauto.
-    + move=> s t h st u la. apply: (p_cl _ (s := App s u))...
+    + move=> s t h st u la. apply: (p_cl _ (s := App s u)); eauto using step.
     + move=> s ns h t la. have snt := p_sn (ih1 _ safe) la.
-      elim: snt la => {} t _ ih3 la. apply: p_nc... move=> v st. inv st=> //...
+      elim: snt la => {} t _ ih3 la; eauto using step. apply: p_nc. move=> v st. inv st=> //; eauto using step.
       apply: ih3 => //. exact: (p_cl (ih1 _ safe)) la _.
   - constructor.
     + move=> s /(_ sn (TyVar 0) reducible_sn)/p_sn/sn_tclosed; apply.
-      by apply/ih/ad_cons...
-    + move=> s t h st P B rep. apply: p_cl (step_tapp B st)...
+      by apply/ih/ad_cons; eauto using step.
+    + move=> s t h st P B rep. apply: p_cl (step_tapp B st); eauto using step.
       by apply/ih/ad_cons.
-    + move=> s ns h P B rep. apply ih... exact: ad_cons.
-      move=> t st. inv st => //...
+    + move=> s ns h P B rep. apply ih; eauto using step. exact: ad_cons.
+      move=> t st. inv st => //; eauto using step.
 Qed.
 
 Corollary L_sn A rho s : admissible rho -> L A rho s -> sn s.
@@ -249,7 +249,7 @@ Proof. move=> /L_cl cl H st. elim: st H; eauto. Qed.
 Lemma beta_expansion A B rho s t :
   admissible rho -> sn t -> L A rho s.[t/] ->
   L A rho (App (Abs B s) t).
-Proof with eauto.
+Proof.
   move=> ad snt h. have sns := sn_subst (L_sn ad h).
   elim: sns t snt h => {} s sns ih1 t. elim=> {} t snt ih2 h.
   apply: L_nc => // u st. inv st => //.
@@ -286,7 +286,7 @@ Qed.
 
 Lemma L_ren A rho xi s :
   L A.[ren xi] rho s <-> L A (xi >>> rho) s.
-Proof with intuition.
+Proof.
   elim: A rho xi s => [x|A ih1 B ih2|A ih] rho xi s; asimpl => //.
   - split=> h1 t h2. rewrite -ih2. apply: h1. by rewrite ih1.
     rewrite ih2. apply: h1. by rewrite -ih1.
@@ -312,12 +312,12 @@ Qed.
 Theorem soundness Gamma s A :
   has_type Gamma s A -> forall rho theta sigma,
     admissible rho -> EL Gamma rho sigma -> L A rho s.|[theta].[sigma].
-Proof with eauto using L_sn, ad_cons.
+Proof.
   elim=> {Gamma s A} [|Gamma A B s _ ih||Gamma A s _ ih|Gamma A B s _ /=ih]
-    rho theta sigma ad el; asimpl...
-  - move=> t h. apply: beta_expansion... asimpl. apply: ih... by case.
-  - move=> P B h. apply: inst_expansion... asimpl. apply: ih... move=> x.
-    rewrite size_map => lt. rewrite get_map // L_weaken...
+    rho theta sigma ad el; asimpl; eauto using L_sn, ad_con.
+  - move=> t h. apply: beta_expansion; eauto using L_sn, ad_con. asimpl. apply: ih; eauto using L_sn, ad_con. by case.
+  - move=> P B h. apply: inst_expansion; eauto using L_sn, ad_con. asimpl. apply: ih; eauto using L_sn, ad_con. move=> x.
+    rewrite size_map => lt. rewrite get_map // L_weaken; eauto using L_sn, ad_con.
   - rewrite L_subst. specialize (ih _ theta sigma ad el (L B rho) B.[theta]).
     have/ih: reducible (L B rho). exact: L_reducible. apply L_ext. by case.
 Qed.
diff --git a/examples/ssr/pred_CC_omega.v b/examples/ssr/pred_CC_omega.v
index fae03f0..0ab908a 100644
--- a/examples/ssr/pred_CC_omega.v
+++ b/examples/ssr/pred_CC_omega.v
@@ -180,10 +180,10 @@ Qed.
 
 Lemma pstep_compat sigma tau s t :
   psstep sigma tau -> pstep s t -> pstep s.[sigma] t.[tau].
-Proof with eauto using pstep, psstep_up.
-  move=> A B. elim: B sigma tau A; asimpl...
+Proof.
+  move=> A B. elim: B sigma tau A; asimpl; eauto using pstep, psstep_up.
   move=> s1 s2 t1 t2 u -> _ A _ B sigma tau C.
-  apply: (@pstep_beta _ (s2.[up tau]) _ (t2.[tau])); asimpl...
+  apply: (@pstep_beta _ (s2.[up tau]) _ (t2.[tau])); asimpl; eauto using pstep, psstep_up.
 Qed.
 
 Lemma pstep_compat_beta s1 s2 t1 t2 :
@@ -193,11 +193,11 @@ Proof.
 Qed.
 
 Lemma rho_triangle : triangle pstep rho.
-Proof with eauto using pstep.
-  move=> s t. elim=> {s t} //=...
+Proof.
+  move=> s t. elim=> {s t} //=; eauto using pstep.
   - move=> s1 s2 t1 t2 u -> {u} _ A _ B. exact: pstep_compat_beta.
-  - move=> s1 s2 t1 t2 A ih1 _ ih2. case: s1 A ih1 => //=...
-    move=> s A ih1. inv A. inv ih1...
+  - move=> s1 s2 t1 t2 A ih1 _ ih2. case: s1 A ih1 => //=; eauto using pstep.
+    move=> s A ih1. inv A. inv ih1; eauto using pstep.
 Qed.
 
 Theorem church_rosser :
@@ -271,18 +271,18 @@ Proof. move=> leq. exact/sub1_sub/sub1_sort. Qed.
 
 Lemma sub1_trans A B C D :
   sub1 A B -> B === C -> sub1 C D -> A <: D.
-Proof with eauto using sub1, sub1_sub, sub1_conv, conv_sub1.
+Proof.
   move=> sb. elim: sb C D => {A B}
-    [A C D|n m leq C D conv sb|A B1 B2 sb1 ih C D conv sb2]...
-  - inv sb...
+    [A C D|n m leq C D conv sb|A B1 B2 sb1 ih C D conv sb2]; eauto using sub1, sub1_sub, sub1_conv, conv_sub1.
+  - inv sb; eauto using sub1, sub1_sub, sub1_conv, conv_sub1.
     + apply: sub_sort. move: conv => /inj_sort eqn. subst.
       exact: leq_trans leq _.
     + exfalso. exact: conv_prod_sort (conv_sym conv).
-  - inv sb2...
+  - inv sb2; eauto using sub1, sub1_sub, sub1_conv, conv_sub1.
     + exfalso. exact: conv_prod_sort conv.
     + move: conv => /inj_prod[conv1 conv2].
       move: (ih _ _ conv2 H) => {ih} sub. inv sub.
-      eapply SubI. eapply sub1_prod... eapply conv_prod... exact: conv_prod.
+      eapply SubI. eapply sub1_prod; eauto using sub1, sub1_sub, sub1_conv, conv_sub1. eapply conv_prod; eauto using sub1, sub1_sub, sub1_conv, conv_sub1. exact: conv_prod.
 Qed.
 
 Lemma sub_trans B A C :

From 22b82a54797eddd3459325504293b4f6dbf7dcde Mon Sep 17 00:00:00 2001
From: skylee03 <i@skylee.xyz>
Date: Thu, 6 Aug 2026 21:13:48 +0800
Subject: [PATCH 05/24] fix deprecated-syntactic-definition (app_length)

---
 examples/plain/POPLmark.v | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

diff --git a/examples/plain/POPLmark.v b/examples/plain/POPLmark.v
index 3ba96e0..a9ee8ff 100644
--- a/examples/plain/POPLmark.v
+++ b/examples/plain/POPLmark.v
@@ -178,10 +178,10 @@ Proof.
     depind H; intros; simpl in *.
     - constructor.
       eapply wf_weak'. eassumption.
-      repeat rewrite app_length. simpl. lia.
+      repeat rewrite length_app. simpl. lia.
     - constructor. simpl.
       apply atnd_defined. apply atnd_defined in H.
-      repeat rewrite -> app_length in *. simpl in *. lia.
+      repeat rewrite -> length_app in *. simpl in *. lia.
     - decide (x = length Delta').
       + subst.
         econstructor. { apply atnd_repl. }
@@ -194,7 +194,7 @@ Proof.
           rewrite app_assoc.
           replace (S (length Delta')) with (length (Delta' ++ B' :: nil)).
           now apply atnd_steps.
-          rewrite app_length. simpl. lia.
+          rewrite length_app. simpl. lia.
         * asimpl in IHsub.
           eapply IHsub; now eauto.
       + econstructor; eauto.
@@ -203,7 +203,7 @@ Proof.
     - constructor.
       + now eauto.
       + eapply wf_weak'. eassumption.
-        repeat rewrite app_length. simpl. lia.
+        repeat rewrite length_app. simpl. lia.
       + change (B1 :: Delta' ++ B' :: Delta)
           with ((B1 :: Delta') ++ B' :: Delta).
         eapply IHsub2; eauto.
@@ -340,10 +340,10 @@ Lemma ty_narrow Delta2 Delta1 Gamma A B C s:
   TY Delta2 ++ A :: Delta1 ; Gamma |- s : C.
 Proof.
   intros H. depind H; econstructor; eauto using ty.
-  - eapply wf_weak'. eassumption. repeat rewrite app_length. simpl. lia.
+  - eapply wf_weak'. eassumption. repeat rewrite length_app. simpl. lia.
   - change (A0 :: Delta2 ++ A :: Delta1) with ((A0 :: Delta2) ++ A :: Delta1).
     eapply IHty. reflexivity. assumption.
-  - eapply wf_weak'. eassumption. repeat rewrite app_length. simpl. lia.
+  - eapply wf_weak'. eassumption. repeat rewrite length_app. simpl. lia.
   - now eapply sub_narrow; eauto.
   - now eapply sub_narrow; eauto.
 Qed.

From 4e4a6a9af9645965dd55d5c7d496f6e4410152ff Mon Sep 17 00:00:00 2001
From: skylee03 <i@skylee.xyz>
Date: Thu, 6 Aug 2026 21:18:26 +0800
Subject: [PATCH 06/24] fix notation-for-abbreviation

---
 examples/ssr/BetaSubstitution.v | 4 ++--
 examples/ssr/CR.v               | 2 +-
 examples/ssr/SystemF_CBV.v      | 2 +-
 examples/ssr/SystemF_SN.v       | 2 +-
 examples/ssr/pred_CC_omega.v    | 2 +-
 5 files changed, 6 insertions(+), 6 deletions(-)

diff --git a/examples/ssr/BetaSubstitution.v b/examples/ssr/BetaSubstitution.v
index 43188a7..f0764ab 100644
--- a/examples/ssr/BetaSubstitution.v
+++ b/examples/ssr/BetaSubstitution.v
@@ -25,7 +25,7 @@ Fixpoint lift_at (d k : nat) (s : term) : term :=
     | App s t => App (lift_at d k s) (lift_at d k t)
     | Lam s   => Lam (lift_at d.+1 k s)
   end.
-Notation lift := (lift_at 0).
+Abbreviation lift := (lift_at 0).
 
 Fixpoint sbst_at (d : nat) (t s : term) : term :=
   match s with
@@ -33,7 +33,7 @@ Fixpoint sbst_at (d : nat) (t s : term) : term :=
     | App s1 s2 => App (sbst_at d t s1) (sbst_at d t s2)
     | Lam s => Lam (sbst_at d.+1 t s)
   end.
-Notation sbst := (sbst_at 0).
+Abbreviation sbst := (sbst_at 0).
 
 (** Soundness proof *)
 
diff --git a/examples/ssr/CR.v b/examples/ssr/CR.v
index 25b5f63..8dda12d 100644
--- a/examples/ssr/CR.v
+++ b/examples/ssr/CR.v
@@ -30,7 +30,7 @@ Inductive step : term -> term -> Prop :=
 | step_lam s1 s2 :
     step s1 s2 -> step (Lam s1) (Lam s2).
 
-Notation red := (star step).
+Abbreviation red := (star step).
 Notation "s === t" := (conv step s t) (at level 50).
 
 (*
diff --git a/examples/ssr/SystemF_CBV.v b/examples/ssr/SystemF_CBV.v
index c3dbea7..10f3500 100644
--- a/examples/ssr/SystemF_CBV.v
+++ b/examples/ssr/SystemF_CBV.v
@@ -88,7 +88,7 @@ Fixpoint V (A : type) (rho : var -> term -> Prop) (v : term) {struct A} : Prop :
     | All A => exists2 s : term, v = TAbs s &
         forall i (B : type), L (V A (i .: rho)) s.|[B/]
   end.
-Notation E A rho := (L (V A rho)).
+Abbreviation E A rho := (L (V A rho)).
 
 Lemma V_value A rho v : V A rho v -> eval v v.
 Proof. by elim: A => [x[]|A _ B _/=[A'[s->]]|A _/=[s->]]. Qed.
diff --git a/examples/ssr/SystemF_SN.v b/examples/ssr/SystemF_SN.v
index 65d3b6b..ca099b8 100644
--- a/examples/ssr/SystemF_SN.v
+++ b/examples/ssr/SystemF_SN.v
@@ -151,7 +151,7 @@ Inductive has_type (Gamma : ctx) : term -> type -> Prop :=
 
 (* Strong Normalization *)
 
-Notation sn := (sn step).
+Abbreviation sn := (sn step).
 
 Lemma sn_closed t s : sn (App s t) -> sn s.
 Proof. apply: (sn_preimage (h := App^~t)) => x y. exact: step_appL. Qed.
diff --git a/examples/ssr/pred_CC_omega.v b/examples/ssr/pred_CC_omega.v
index 0ab908a..4a72542 100644
--- a/examples/ssr/pred_CC_omega.v
+++ b/examples/ssr/pred_CC_omega.v
@@ -39,7 +39,7 @@ Inductive step : term -> term -> Prop :=
 | step_prodR A B1 B2 :
     step B1 B2 -> step (Prod A B1) (Prod A B2).
 
-Notation red := (star step).
+Abbreviation red := (star step).
 Notation "s === t" := (conv step s t) (at level 50).
 
 Definition sred sigma tau :=

From b18a8b4e13a6f29ee5dc19f1acb0fafccf437a01 Mon Sep 17 00:00:00 2001
From: skylee03 <i@skylee.xyz>
Date: Thu, 6 Aug 2026 21:27:56 +0800
Subject: [PATCH 07/24] fix deprecated-from-Coq

---
 examples/ssr/AutosubstSsr.v  | 2 +-
 examples/ssr/CR.v            | 2 +-
 examples/ssr/SystemF_SN.v    | 2 +-
 examples/ssr/pred_CC_omega.v | 2 +-
 4 files changed, 4 insertions(+), 4 deletions(-)

diff --git a/examples/ssr/AutosubstSsr.v b/examples/ssr/AutosubstSsr.v
index 04600e7..a857f8c 100644
--- a/examples/ssr/AutosubstSsr.v
+++ b/examples/ssr/AutosubstSsr.v
@@ -6,7 +6,7 @@ Require Export Autosubst.Autosubst_Tactics.
 Require Export Autosubst.Autosubst_Lemmas.
 Require Export Autosubst.Autosubst_Derive.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq.
-From Coq Require Import ssrfun.
+From Stdlib Require Import ssrfun.
 
 Set Implicit Arguments.
 Unset Strict Implicit.
diff --git a/examples/ssr/CR.v b/examples/ssr/CR.v
index 8dda12d..4418275 100644
--- a/examples/ssr/CR.v
+++ b/examples/ssr/CR.v
@@ -1,5 +1,5 @@
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq.
-From Coq Require Import ssrfun.
+From Stdlib Require Import ssrfun.
 Require Import AutosubstSsr ARS.
 
 Set Implicit Arguments.
diff --git a/examples/ssr/SystemF_SN.v b/examples/ssr/SystemF_SN.v
index ca099b8..f7acec4 100644
--- a/examples/ssr/SystemF_SN.v
+++ b/examples/ssr/SystemF_SN.v
@@ -1,7 +1,7 @@
 (** * Strong Normalization of System F *)
 
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq.
-From Coq Require Import ssrfun.
+From Stdlib Require Import ssrfun.
 Require Import AutosubstSsr ARS Context.
 
 Set Implicit Arguments.
diff --git a/examples/ssr/pred_CC_omega.v b/examples/ssr/pred_CC_omega.v
index 4a72542..1f9ab2b 100644
--- a/examples/ssr/pred_CC_omega.v
+++ b/examples/ssr/pred_CC_omega.v
@@ -2,7 +2,7 @@
  *)
 
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq.
-From Coq Require Import ssrfun.
+From Stdlib Require Import ssrfun.
 Require Import AutosubstSsr ARS Context.
 
 Set Implicit Arguments.

From b878ba74c081815885e44ee121335174a93f81cc Mon Sep 17 00:00:00 2001
From: skylee03 <i@skylee.xyz>
Date: Thu, 6 Aug 2026 21:38:17 +0800
Subject: [PATCH 08/24] fix implicit-create-hint-db and
 implicit-create-rewrite-hint-db

---
 examples/plain/Makefile      | 2 +-
 examples/plain/Size.v        | 3 +++
 examples/ssr/CR.v            | 1 +
 examples/ssr/Makefile        | 2 +-
 examples/ssr/SystemF_SN.v    | 1 +
 examples/ssr/pred_CC_omega.v | 1 +
 theories/Autosubst_MMap.v    | 4 ++++
 theories/Makefile            | 2 +-
 8 files changed, 13 insertions(+), 3 deletions(-)

diff --git a/examples/plain/Makefile b/examples/plain/Makefile
index 17ced67..030d13d 100644
--- a/examples/plain/Makefile
+++ b/examples/plain/Makefile
@@ -8,7 +8,7 @@ all: $(COQMAKEFILE)
 	+$(MAKE) -f $(COQMAKEFILE) all
 
 $(COQMAKEFILE): Makefile $(VS)
-	rocq makefile -R $(LIB) Autosubst -R . Plain $(VS) -o $(COQMAKEFILE)
+	rocq makefile -R $(LIB) Autosubst -R . Plain $(VS) -o $(COQMAKEFILE) -arg "-w -notation-overridden"
 
 clean: $(COQMAKEFILE)
 	-$(COQMAKE) clean
diff --git a/examples/plain/Size.v b/examples/plain/Size.v
index ba335b2..24017c3 100644
--- a/examples/plain/Size.v
+++ b/examples/plain/Size.v
@@ -31,6 +31,7 @@ Ltac derive_Size :=
     end
   end.
 
+Create HintDb derive.
 Global Hint Extern 0 (Size _) => derive_Size : derive.
 
 Lemma size_rec {A : Type} f (x : A) :
@@ -93,6 +94,8 @@ Arguments size_fact {A} x {P _}.
 Lemma size_app (A : Type) (size_A : Size A) l1 l2 :
   size (app l1 l2) = size l1 + size l2.
 Proof. induction l1; simpl; intuition (auto with zarith). Qed.
+
+Create Rewrite HintDb size.
 Global Hint Rewrite @size_app : size.
 
 Global Instance size_fact_app (A : Type) (size_A : Size A) l1 l2 :
diff --git a/examples/ssr/CR.v b/examples/ssr/CR.v
index 4418275..26325be 100644
--- a/examples/ssr/CR.v
+++ b/examples/ssr/CR.v
@@ -57,6 +57,7 @@ Qed.
 Lemma red_lam s1 s2 : red s1 s2 -> red (Lam s1) (Lam s2).
 Proof. apply: star_hom => x y. exact: step_lam. Qed.
 
+Create HintDb red_congr.
 Global Hint Resolve red_app red_lam : red_congr.
 
 (** **** Church-Rosser theorem *)
diff --git a/examples/ssr/Makefile b/examples/ssr/Makefile
index b12f601..dc82945 100644
--- a/examples/ssr/Makefile
+++ b/examples/ssr/Makefile
@@ -8,7 +8,7 @@ all: $(COQMAKEFILE)
 	+$(MAKE) -f $(COQMAKEFILE) all
 
 $(COQMAKEFILE): Makefile $(VS)
-	rocq makefile -R $(LIB) Autosubst $(VS) -R . Ssr -o $(COQMAKEFILE)
+	rocq makefile -R $(LIB) Autosubst $(VS) -R . Ssr -o $(COQMAKEFILE) -arg "-w -notation-overridden"
 
 clean: $(COQMAKEFILE)
 	-$(COQMAKE) clean
diff --git a/examples/ssr/SystemF_SN.v b/examples/ssr/SystemF_SN.v
index f7acec4..c9fce34 100644
--- a/examples/ssr/SystemF_SN.v
+++ b/examples/ssr/SystemF_SN.v
@@ -116,6 +116,7 @@ Lemma sred_hup sigma tau theta :
   sred sigma tau -> sred (sigma >>| theta) (tau >>| theta).
 Proof. move=> A n /=. apply/red_hsubst/A. Qed.
 
+Create HintDb red_congr.
 Global Hint Resolve red_app red_abs red_tapp red_tabs sred_up sred_hup : red_congr.
 
 Lemma red_compat sigma tau s :
diff --git a/examples/ssr/pred_CC_omega.v b/examples/ssr/pred_CC_omega.v
index 1f9ab2b..4d51169 100644
--- a/examples/ssr/pred_CC_omega.v
+++ b/examples/ssr/pred_CC_omega.v
@@ -78,6 +78,7 @@ Proof. apply: star_hom. exact: step_subst. Qed.
 Lemma sred_up sigma tau : sred sigma tau -> sred (up sigma) (up tau).
 Proof. move=> A [|n] //=. asimpl. apply: red_subst. exact: A. Qed.
 
+Create HintDb red_congr.
 Global Hint Resolve red_app red_lam red_prod sred_up : red_congr.
 
 Lemma red_compat sigma tau s : sred sigma tau -> red s.[sigma] s.[tau].
diff --git a/theories/Autosubst_MMap.v b/theories/Autosubst_MMap.v
index 5d75b28..5e1b480 100644
--- a/theories/Autosubst_MMap.v
+++ b/theories/Autosubst_MMap.v
@@ -94,10 +94,12 @@ Ltac mmap_typeclass_normalizeH H :=
      let s := constr:(@mmap A B _ f) in progress change (@mmap A B _ f) with s
   end.
 
+Create Rewrite HintDb mmap.
 Global Hint Rewrite @mmap_id_instE @mmap_const_instE : mmap.
 Global Hint Rewrite @mmap_id @mmap_comp @mmap_idX @mmap_compX @mmap_compR
   using exact _ : mmap.
 
+Create Rewrite HintDb autosubst.
 Global Hint Rewrite @mmap_id_instE @mmap_const_instE : autosubst.
 Global Hint Rewrite @mmap_id @mmap_comp @mmap_idX @mmap_compX @mmap_compR
   using exact _ : autosubst.
@@ -144,6 +146,8 @@ Ltac derive_MMap :=
         let ys := tmap ys in exact ys
     end
   end.
+
+Create HintDb derive.
 Global Hint Extern 0 (MMap _ _) => derive_MMap : derive.
 
 Ltac derive_MMapLemmas := constructor;
diff --git a/theories/Makefile b/theories/Makefile
index e182f73..493b49f 100644
--- a/theories/Makefile
+++ b/theories/Makefile
@@ -8,7 +8,7 @@ all: $(COQMAKEFILE)
 	+$(MAKE) -f $(COQMAKEFILE) all
 
 $(COQMAKEFILE): Makefile $(VS)
-	rocq makefile -R $(LIB) Autosubst $(VS) -o $(COQMAKEFILE)
+	rocq makefile -R $(LIB) Autosubst $(VS) -o $(COQMAKEFILE) -arg "-w -notation-overridden"
 
 install: $(COQMAKEFILE)
 	$(COQMAKE) install

From 6e759af0193d3e40d432f7e894af052ee4c93925 Mon Sep 17 00:00:00 2001
From: skylee03 <i@skylee.xyz>
Date: Thu, 6 Aug 2026 21:48:13 +0800
Subject: [PATCH 09/24] fix L_reducible

---
 examples/ssr/SystemF_SN.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/examples/ssr/SystemF_SN.v b/examples/ssr/SystemF_SN.v
index c9fce34..523fab2 100644
--- a/examples/ssr/SystemF_SN.v
+++ b/examples/ssr/SystemF_SN.v
@@ -217,7 +217,7 @@ Proof.
       eapply h. eapply reducible_var; eauto.
     + move=> s t h st u la. apply: (p_cl _ (s := App s u)); eauto using step.
     + move=> s ns h t la. have snt := p_sn (ih1 _ safe) la.
-      elim: snt la => {} t _ ih3 la; eauto using step. apply: p_nc. move=> v st. inv st=> //; eauto using step.
+      elim: snt la => {} t _ ih3 la; eauto using step. apply: p_nc; eauto using step. move=> v st. inv st=> //; eauto using step.
       apply: ih3 => //. exact: (p_cl (ih1 _ safe)) la _.
   - constructor.
     + move=> s /(_ sn (TyVar 0) reducible_sn)/p_sn/sn_tclosed; apply.

From bff1971b2ef7881b003aff17592367e68ef92e05 Mon Sep 17 00:00:00 2001
From: skylee03 <i@skylee.xyz>
Date: Thu, 6 Aug 2026 21:49:20 +0800
Subject: [PATCH 10/24] fix SystemF_SN.soundness

---
 examples/ssr/SystemF_SN.v | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/examples/ssr/SystemF_SN.v b/examples/ssr/SystemF_SN.v
index 523fab2..6161dab 100644
--- a/examples/ssr/SystemF_SN.v
+++ b/examples/ssr/SystemF_SN.v
@@ -315,10 +315,10 @@ Theorem soundness Gamma s A :
     admissible rho -> EL Gamma rho sigma -> L A rho s.|[theta].[sigma].
 Proof.
   elim=> {Gamma s A} [|Gamma A B s _ ih||Gamma A s _ ih|Gamma A B s _ /=ih]
-    rho theta sigma ad el; asimpl; eauto using L_sn, ad_con.
-  - move=> t h. apply: beta_expansion; eauto using L_sn, ad_con. asimpl. apply: ih; eauto using L_sn, ad_con. by case.
-  - move=> P B h. apply: inst_expansion; eauto using L_sn, ad_con. asimpl. apply: ih; eauto using L_sn, ad_con. move=> x.
-    rewrite size_map => lt. rewrite get_map // L_weaken; eauto using L_sn, ad_con.
+    rho theta sigma ad el; asimpl; eauto using L_sn, ad_cons.
+  - move=> t h. apply: beta_expansion; eauto using L_sn, ad_cons. asimpl. apply: ih; eauto using L_sn, ad_cons. by case.
+  - move=> P B h. apply: inst_expansion; eauto using L_sn, ad_cons. asimpl. apply: ih; eauto using L_sn, ad_cons. move=> x.
+    rewrite size_map => lt. rewrite get_map // L_weaken; eauto using L_sn, ad_cons.
   - rewrite L_subst. specialize (ih _ theta sigma ad el (L B rho) B.[theta]).
     have/ih: reducible (L B rho). exact: L_reducible. apply L_ext. by case.
 Qed.

From b3304ad7bc03833e6e61199c92d6d1334832febc Mon Sep 17 00:00:00 2001
From: skylee03 <i@skylee.xyz>
Date: Thu, 6 Aug 2026 21:54:31 +0800
Subject: [PATCH 11/24] unhide warnings

---
 examples/plain/Makefile | 2 +-
 examples/ssr/Makefile   | 2 +-
 theories/Makefile       | 2 +-
 3 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/examples/plain/Makefile b/examples/plain/Makefile
index 030d13d..17ced67 100644
--- a/examples/plain/Makefile
+++ b/examples/plain/Makefile
@@ -8,7 +8,7 @@ all: $(COQMAKEFILE)
 	+$(MAKE) -f $(COQMAKEFILE) all
 
 $(COQMAKEFILE): Makefile $(VS)
-	rocq makefile -R $(LIB) Autosubst -R . Plain $(VS) -o $(COQMAKEFILE) -arg "-w -notation-overridden"
+	rocq makefile -R $(LIB) Autosubst -R . Plain $(VS) -o $(COQMAKEFILE)
 
 clean: $(COQMAKEFILE)
 	-$(COQMAKE) clean
diff --git a/examples/ssr/Makefile b/examples/ssr/Makefile
index dc82945..b12f601 100644
--- a/examples/ssr/Makefile
+++ b/examples/ssr/Makefile
@@ -8,7 +8,7 @@ all: $(COQMAKEFILE)
 	+$(MAKE) -f $(COQMAKEFILE) all
 
 $(COQMAKEFILE): Makefile $(VS)
-	rocq makefile -R $(LIB) Autosubst $(VS) -R . Ssr -o $(COQMAKEFILE) -arg "-w -notation-overridden"
+	rocq makefile -R $(LIB) Autosubst $(VS) -R . Ssr -o $(COQMAKEFILE)
 
 clean: $(COQMAKEFILE)
 	-$(COQMAKE) clean
diff --git a/theories/Makefile b/theories/Makefile
index 493b49f..e182f73 100644
--- a/theories/Makefile
+++ b/theories/Makefile
@@ -8,7 +8,7 @@ all: $(COQMAKEFILE)
 	+$(MAKE) -f $(COQMAKEFILE) all
 
 $(COQMAKEFILE): Makefile $(VS)
-	rocq makefile -R $(LIB) Autosubst $(VS) -o $(COQMAKEFILE) -arg "-w -notation-overridden"
+	rocq makefile -R $(LIB) Autosubst $(VS) -o $(COQMAKEFILE)
 
 install: $(COQMAKEFILE)
 	$(COQMAKE) install

From 8537546bf2426a6ffba05f147890d0f6bea0a7d0 Mon Sep 17 00:00:00 2001
From: skylee03 <i@skylee.xyz>
Date: Thu, 6 Aug 2026 22:23:03 +0800
Subject: [PATCH 12/24] simplify eautos

---
 examples/ssr/CR.v            | 18 +++++++++---------
 examples/ssr/POPLmark.v      | 26 +++++++++++++-------------
 examples/ssr/SystemF_SN.v    | 24 ++++++++++++------------
 examples/ssr/pred_CC_omega.v | 10 +++++-----
 4 files changed, 39 insertions(+), 39 deletions(-)

diff --git a/examples/ssr/CR.v b/examples/ssr/CR.v
index 26325be..26186f5 100644
--- a/examples/ssr/CR.v
+++ b/examples/ssr/CR.v
@@ -96,15 +96,15 @@ Proof. elim; eauto using pstep. Qed.
 
 Lemma pstep_red s t : pstep s t -> red s t.
 Proof.
-  elim=> {s t} //=; eauto with red_congr. move=> s1 s2 t1 t2 _ A _ B.
-  apply: (star_trans (App (Lam s2) t2)); eauto with red_congr. exact/star1/step_beta.
+  elim=> {s t} //=; auto with red_congr. move=> s1 s2 t1 t2 _ A _ B.
+  apply: (star_trans (App (Lam s2) t2)); auto with red_congr. exact/star1/step_beta.
 Qed.
 
 Lemma pstep_subst sigma s t :
   pstep s t -> pstep s.[sigma] t.[sigma].
 Proof.
-  move=> A. elim: A sigma => /=; eauto using pstep. move=> s1 s2 t1 t2 _ A _ B sigma.
-  eapply pstep_ebeta; eauto using pstep. by autosubst.
+  move=> A. elim: A sigma => /=; auto using pstep. move=> s1 s2 t1 t2 _ A _ B sigma.
+  eapply pstep_ebeta => //. by autosubst.
 Qed.
 
 Lemma psstep_up sigma tau :
@@ -116,9 +116,9 @@ Qed.
 Lemma pstep_compat sigma tau s t :
   psstep sigma tau -> pstep s t -> pstep s.[sigma] t.[tau].
 Proof.
-  move=> A B. elim: B sigma tau A; asimpl; eauto using pstep, psstep_up.
+  move=> A B. elim: B sigma tau A; asimpl; auto using pstep, psstep_up.
   move=> s1 s2 t1 t2 _ A _ B sigma tau C.
-  apply: (@pstep_ebeta _ (s2.[up tau]) _ (t2.[tau])); asimpl; eauto using pstep, psstep_up.
+  apply: (@pstep_ebeta _ (s2.[up tau]) _ (t2.[tau])); asimpl; auto using psstep_up.
 Qed.
 
 Lemma pstep_compat_beta s1 s2 t1 t2 :
@@ -129,10 +129,10 @@ Qed.
 
 Lemma rho_triangle : triangle pstep rho.
 Proof.
-  move=> s t. elim=> {s t} //=; eauto using pstep.
+  move=> s t. elim=> {s t} //=; auto using pstep.
   - move=> s1 s2 t1 t2 _ A _ B. exact: pstep_compat_beta.
-  - move=> s1 s2 t1 t2 A ih1 _ ih2. case: s1 A ih1 => //=; eauto using pstep.
-    move=> s A ih1. inv A. inv ih1; eauto using pstep.
+  - move=> s1 s2 t1 t2 A ih1 _ ih2. case: s1 A ih1 => //=; auto using pstep.
+    move=> s A ih1. inv A. inv ih1; auto using pstep.
 Qed.
 
 Theorem church_rosser :
diff --git a/examples/ssr/POPLmark.v b/examples/ssr/POPLmark.v
index a564546..ac37248 100644
--- a/examples/ssr/POPLmark.v
+++ b/examples/ssr/POPLmark.v
@@ -106,12 +106,12 @@ Lemma sub_narrow_t Gamma Delta A B :
     Delta`_x = Gamma`_x \/ transitivity_at (Gamma`_x)) ->
   SUB Gamma |- A <: B -> SUB Delta |- A <: B.
 Proof.
-  move=> h1 h2 h3 ty. elim: ty Delta h1 h2 h3 => {Gamma A B} /=; eauto using sub.
-  - move=> Gamma x A lt _ ih Delta h1 h2 h3. apply: sub_var_trans; eauto using sub.
-    case: (h3 x lt) => [->|]; eauto using sub.
-  - move=> Gamma A1 A2 B1 B2 _ ih1 _ ih2 Delta h1 h2 h3. apply: sub_all; eauto using sub.
-    apply: ih2 => [[|x /h1]|[|x /h2/sub_weak]|[_|x /h3[|]]] //=; eauto using sub.
-    move=>->; eauto using sub. move=> tr. right. exact: transitivity_ren.
+  move=> h1 h2 h3 ty. elim: ty Delta h1 h2 h3 => {Gamma A B} /=; auto using sub.
+  - move=> Gamma x A lt _ ih Delta h1 h2 h3. apply: sub_var_trans; auto.
+    case: (h3 x lt) => [->|]; eauto.
+  - move=> Gamma A1 A2 B1 B2 _ ih1 _ ih2 Delta h1 h2 h3. apply: sub_all; auto.
+    apply: ih2 => [[|x /h1]|[|x /h2/sub_weak]|[_|x /h3[|]]] //=; auto.
+    move=>->; auto. move=> tr. right. exact: transitivity_ren.
 Qed.
 
 Definition is_var (A : type) : bool := if A is TyVar _ then true else false.
@@ -121,19 +121,19 @@ Lemma sub_trans_snoc Gamma B C :
     SUB Gamma |- A <: B -> SUB Gamma |- B <: C -> SUB Gamma |- A <: C) ->
   forall A, SUB Gamma |- A <: B -> SUB Gamma |- B <: C -> SUB Gamma |- A <: C.
 Proof.
-  move=> h A ty. elim: ty C h =>{Gamma A B}; eauto using sub. move=> Gamma A C h1 h2. inv h2; eauto using sub.
+  move=> h A ty. elim: ty C h =>{Gamma A B}; auto using sub. move=> Gamma A C h1 h2. inv h2; auto using sub.
 Qed.
 
 Lemma sub_trans_t B : transitivity_at B.
 Proof.
-  elim: B => [x||B1 ih1 B2 ih2|B1 ih1 B2 ih2] Gamma A C xi; asimpl; eauto using sub.
+  elim: B => [x||B1 ih1 B2 ih2|B1 ih1 B2 ih2] Gamma A C xi; asimpl; auto using sub.
   - apply: sub_trans_snoc A => A e ty. by inv ty.
-  - move=> t1 t2. inv t2; eauto using sub.
+  - move=> t1 t2. inv t2; auto using sub.
   - apply: sub_trans_snoc A => A e ty1 ty2. inv ty1 => //. inv ty2; eauto using sub.
   - apply: sub_trans_snoc A => A e ty1 ty2. inv ty1 => //. inv ty2; eauto using sub.
-    apply: sub_all; eauto using sub. eapply ih2; eauto using sub. move: H3. apply: sub_narrow_t; eauto using sub.
+    apply: sub_all; eauto. eapply ih2; eauto. move: H3. apply: sub_narrow_t; auto using sub.
     + case=> //= _. exact: sub_weak.
-    + move=> [|x] _; eauto using sub. right => /=. asimpl. exact: transitivity_ren.
+    + move=> [|x] _; auto. right => /=. asimpl. exact: transitivity_ren.
 Qed.
 
 Corollary sub_trans Gamma A B C :
@@ -155,7 +155,7 @@ Lemma sub_subst Gamma Delta A B sigma :
 Proof.
   move=> h ty. elim: ty Delta sigma h => {A B} Gamma; eauto using sub.
   - move=> x A lt _ ih Delta sigma h /=. apply: sub_trans (h _ lt) _. exact: ih.
-  - move=> A1 A2 B1 B2 _ ih1 _ ih2 Delta sigma h /=. apply: sub_all; eauto using sub.
+  - move=> A1 A2 B1 B2 _ ih1 _ ih2 Delta sigma h /=. apply: sub_all; auto.
     apply: ih2 => -[_|x /h/sub_weak]. apply: sub_var_trans => //. autosubst.
     autosubst.
 Qed.
@@ -223,7 +223,7 @@ Lemma ty_ren Delta Gamma1 Gamma2 s A xi :
   TY Delta;Gamma1 |- s : A -> TY Delta;Gamma2 |- s.[ren xi] : A.
 Proof.
   move=> h1 h2 ty. elim: ty Gamma2 xi h1 h2 => {Delta Gamma1 s A} /=; eauto using ty.
-  - move=> Delta Gamma1 x lt Gamma2 xi h1 h2. rewrite -h2 //. apply: ty_var; eauto using ty.
+  - move=> Delta Gamma1 x lt Gamma2 xi h1 h2. rewrite -h2 //. apply: ty_var; eauto.
   - move=> Delta Gamma1 A B s _ ih Gamma2 xi h1 h2. asimpl. apply: ty_abs.
     by apply: ih => [[|x/h1]|[|x/h2]].
   - move=> Delta Gamma1 A B s _ ih Gamma2 xi h1 h2. apply: ty_tabs.
diff --git a/examples/ssr/SystemF_SN.v b/examples/ssr/SystemF_SN.v
index 6161dab..aee7328 100644
--- a/examples/ssr/SystemF_SN.v
+++ b/examples/ssr/SystemF_SN.v
@@ -211,21 +211,21 @@ Proof. by move=> H1 H2 [|i] //=. Qed.
 Lemma L_reducible T rho :
   admissible rho -> reducible (L T rho).
 Proof.
-  elim: T rho => /=[i|A ih1 B ih2|A ih] rho safe; eauto using step.
+  elim: T rho => /=[i|A ih1 B ih2|A ih] rho safe; auto.
   - constructor.
-    + move=> s h. apply: (@sn_closed (TeVar 0)). apply: (p_sn (P := L B rho)); eauto using step.
+    + move=> s h. apply: (@sn_closed (TeVar 0)). apply: (p_sn (P := L B rho)); auto.
       eapply h. eapply reducible_var; eauto.
-    + move=> s t h st u la. apply: (p_cl _ (s := App s u)); eauto using step.
+    + move=> s t h st u la. apply: (p_cl _ (s := App s u)); auto using step.
     + move=> s ns h t la. have snt := p_sn (ih1 _ safe) la.
-      elim: snt la => {} t _ ih3 la; eauto using step. apply: p_nc; eauto using step. move=> v st. inv st=> //; eauto using step.
+      elim: snt la => {} t _ ih3 la; auto. apply: p_nc; auto. move=> v st. inv st=> //; auto.
       apply: ih3 => //. exact: (p_cl (ih1 _ safe)) la _.
   - constructor.
     + move=> s /(_ sn (TyVar 0) reducible_sn)/p_sn/sn_tclosed; apply.
-      by apply/ih/ad_cons; eauto using step.
-    + move=> s t h st P B rep. apply: p_cl (step_tapp B st); eauto using step.
       by apply/ih/ad_cons.
-    + move=> s ns h P B rep. apply ih; eauto using step. exact: ad_cons.
-      move=> t st. inv st => //; eauto using step.
+    + move=> s t h st P B rep. apply: p_cl (step_tapp B st); auto.
+      by apply/ih/ad_cons.
+    + move=> s ns h P B rep. apply ih; auto. exact: ad_cons.
+      move=> t st. inv st => //; auto.
 Qed.
 
 Corollary L_sn A rho s : admissible rho -> L A rho s -> sn s.
@@ -315,10 +315,10 @@ Theorem soundness Gamma s A :
     admissible rho -> EL Gamma rho sigma -> L A rho s.|[theta].[sigma].
 Proof.
   elim=> {Gamma s A} [|Gamma A B s _ ih||Gamma A s _ ih|Gamma A B s _ /=ih]
-    rho theta sigma ad el; asimpl; eauto using L_sn, ad_cons.
-  - move=> t h. apply: beta_expansion; eauto using L_sn, ad_cons. asimpl. apply: ih; eauto using L_sn, ad_cons. by case.
-  - move=> P B h. apply: inst_expansion; eauto using L_sn, ad_cons. asimpl. apply: ih; eauto using L_sn, ad_cons. move=> x.
-    rewrite size_map => lt. rewrite get_map // L_weaken; eauto using L_sn, ad_cons.
+    rho theta sigma ad el; asimpl; eauto using ad_cons.
+  - move=> t h. apply: beta_expansion; eauto using L_sn. asimpl. apply: ih; auto. by case.
+  - move=> P B h. apply: inst_expansion; eauto using ad_cons. asimpl. apply: ih; auto using ad_cons. move=> x.
+    rewrite size_map => lt. rewrite get_map // L_weaken; eauto.
   - rewrite L_subst. specialize (ih _ theta sigma ad el (L B rho) B.[theta]).
     have/ih: reducible (L B rho). exact: L_reducible. apply L_ext. by case.
 Qed.
diff --git a/examples/ssr/pred_CC_omega.v b/examples/ssr/pred_CC_omega.v
index 4d51169..16396df 100644
--- a/examples/ssr/pred_CC_omega.v
+++ b/examples/ssr/pred_CC_omega.v
@@ -184,7 +184,7 @@ Lemma pstep_compat sigma tau s t :
 Proof.
   move=> A B. elim: B sigma tau A; asimpl; eauto using pstep, psstep_up.
   move=> s1 s2 t1 t2 u -> _ A _ B sigma tau C.
-  apply: (@pstep_beta _ (s2.[up tau]) _ (t2.[tau])); asimpl; eauto using pstep, psstep_up.
+  apply: (@pstep_beta _ (s2.[up tau]) _ (t2.[tau])); asimpl; eauto using psstep_up.
 Qed.
 
 Lemma pstep_compat_beta s1 s2 t1 t2 :
@@ -274,16 +274,16 @@ Lemma sub1_trans A B C D :
   sub1 A B -> B === C -> sub1 C D -> A <: D.
 Proof.
   move=> sb. elim: sb C D => {A B}
-    [A C D|n m leq C D conv sb|A B1 B2 sb1 ih C D conv sb2]; eauto using sub1, sub1_sub, sub1_conv, conv_sub1.
-  - inv sb; eauto using sub1, sub1_sub, sub1_conv, conv_sub1.
+    [A C D|n m leq C D conv sb|A B1 B2 sb1 ih C D conv sb2]; eauto using conv_sub1.
+  - inv sb; eauto using sub1, sub1_conv.
     + apply: sub_sort. move: conv => /inj_sort eqn. subst.
       exact: leq_trans leq _.
     + exfalso. exact: conv_prod_sort (conv_sym conv).
-  - inv sb2; eauto using sub1, sub1_sub, sub1_conv, conv_sub1.
+  - inv sb2; eauto using sub1, sub1_conv.
     + exfalso. exact: conv_prod_sort conv.
     + move: conv => /inj_prod[conv1 conv2].
       move: (ih _ _ conv2 H) => {ih} sub. inv sub.
-      eapply SubI. eapply sub1_prod; eauto using sub1, sub1_sub, sub1_conv, conv_sub1. eapply conv_prod; eauto using sub1, sub1_sub, sub1_conv, conv_sub1. exact: conv_prod.
+      eapply SubI. eapply sub1_prod; eauto. eapply conv_prod => //. exact: conv_prod.
 Qed.
 
 Lemma sub_trans B A C :

From 0565a28ec0f0eed7071f52364d37c857ac80755e Mon Sep 17 00:00:00 2001
From: skylee03 <i@skylee.xyz>
Date: Fri, 7 Aug 2026 21:33:45 +0800
Subject: [PATCH 13/24] unfix implicit-create-hint-db and
 implicit-create-rewrite-hint-db

---
 examples/plain/Size.v        | 2 --
 examples/ssr/CR.v            | 1 -
 examples/ssr/SystemF_SN.v    | 1 -
 examples/ssr/pred_CC_omega.v | 1 -
 theories/Autosubst_MMap.v    | 3 ---
 5 files changed, 8 deletions(-)

diff --git a/examples/plain/Size.v b/examples/plain/Size.v
index 24017c3..a46cca6 100644
--- a/examples/plain/Size.v
+++ b/examples/plain/Size.v
@@ -31,7 +31,6 @@ Ltac derive_Size :=
     end
   end.
 
-Create HintDb derive.
 Global Hint Extern 0 (Size _) => derive_Size : derive.
 
 Lemma size_rec {A : Type} f (x : A) :
@@ -95,7 +94,6 @@ Lemma size_app (A : Type) (size_A : Size A) l1 l2 :
   size (app l1 l2) = size l1 + size l2.
 Proof. induction l1; simpl; intuition (auto with zarith). Qed.
 
-Create Rewrite HintDb size.
 Global Hint Rewrite @size_app : size.
 
 Global Instance size_fact_app (A : Type) (size_A : Size A) l1 l2 :
diff --git a/examples/ssr/CR.v b/examples/ssr/CR.v
index 26186f5..4cc56fa 100644
--- a/examples/ssr/CR.v
+++ b/examples/ssr/CR.v
@@ -57,7 +57,6 @@ Qed.
 Lemma red_lam s1 s2 : red s1 s2 -> red (Lam s1) (Lam s2).
 Proof. apply: star_hom => x y. exact: step_lam. Qed.
 
-Create HintDb red_congr.
 Global Hint Resolve red_app red_lam : red_congr.
 
 (** **** Church-Rosser theorem *)
diff --git a/examples/ssr/SystemF_SN.v b/examples/ssr/SystemF_SN.v
index aee7328..9a58b02 100644
--- a/examples/ssr/SystemF_SN.v
+++ b/examples/ssr/SystemF_SN.v
@@ -116,7 +116,6 @@ Lemma sred_hup sigma tau theta :
   sred sigma tau -> sred (sigma >>| theta) (tau >>| theta).
 Proof. move=> A n /=. apply/red_hsubst/A. Qed.
 
-Create HintDb red_congr.
 Global Hint Resolve red_app red_abs red_tapp red_tabs sred_up sred_hup : red_congr.
 
 Lemma red_compat sigma tau s :
diff --git a/examples/ssr/pred_CC_omega.v b/examples/ssr/pred_CC_omega.v
index 16396df..fa3cafb 100644
--- a/examples/ssr/pred_CC_omega.v
+++ b/examples/ssr/pred_CC_omega.v
@@ -78,7 +78,6 @@ Proof. apply: star_hom. exact: step_subst. Qed.
 Lemma sred_up sigma tau : sred sigma tau -> sred (up sigma) (up tau).
 Proof. move=> A [|n] //=. asimpl. apply: red_subst. exact: A. Qed.
 
-Create HintDb red_congr.
 Global Hint Resolve red_app red_lam red_prod sred_up : red_congr.
 
 Lemma red_compat sigma tau s : sred sigma tau -> red s.[sigma] s.[tau].
diff --git a/theories/Autosubst_MMap.v b/theories/Autosubst_MMap.v
index 5e1b480..c30c63c 100644
--- a/theories/Autosubst_MMap.v
+++ b/theories/Autosubst_MMap.v
@@ -94,12 +94,10 @@ Ltac mmap_typeclass_normalizeH H :=
      let s := constr:(@mmap A B _ f) in progress change (@mmap A B _ f) with s
   end.
 
-Create Rewrite HintDb mmap.
 Global Hint Rewrite @mmap_id_instE @mmap_const_instE : mmap.
 Global Hint Rewrite @mmap_id @mmap_comp @mmap_idX @mmap_compX @mmap_compR
   using exact _ : mmap.
 
-Create Rewrite HintDb autosubst.
 Global Hint Rewrite @mmap_id_instE @mmap_const_instE : autosubst.
 Global Hint Rewrite @mmap_id @mmap_comp @mmap_idX @mmap_compX @mmap_compR
   using exact _ : autosubst.
@@ -147,7 +145,6 @@ Ltac derive_MMap :=
     end
   end.
 
-Create HintDb derive.
 Global Hint Extern 0 (MMap _ _) => derive_MMap : derive.
 
 Ltac derive_MMapLemmas := constructor;

From 29e4c582f5fd9f76f5490582f5528fc25221ae7a Mon Sep 17 00:00:00 2001
From: skylee03 <i@skylee.xyz>
Date: Fri, 7 Aug 2026 21:39:36 +0800
Subject: [PATCH 14/24] silence implicit-create-hint-db and
 implicit-create-rewrite-hint-db

---
 examples/plain/Size.v        | 2 ++
 examples/ssr/CR.v            | 2 ++
 examples/ssr/SystemF_SN.v    | 2 ++
 examples/ssr/pred_CC_omega.v | 2 ++
 theories/Autosubst_MMap.v    | 2 ++
 5 files changed, 10 insertions(+)

diff --git a/examples/plain/Size.v b/examples/plain/Size.v
index a46cca6..b541b4f 100644
--- a/examples/plain/Size.v
+++ b/examples/plain/Size.v
@@ -2,6 +2,8 @@
 From Stdlib Require Import ZArith Lia List Program.Equality.
 Require Import Autosubst.Autosubst_Basics.
 
+Set Warnings "-implicit-create-hint-db, -implicit-create-rewrite-hint-db".
+
 Class Size (A : Type) := size : A -> nat.
 
 Arguments size {A _} !x /.
diff --git a/examples/ssr/CR.v b/examples/ssr/CR.v
index 4cc56fa..c9702af 100644
--- a/examples/ssr/CR.v
+++ b/examples/ssr/CR.v
@@ -6,6 +6,8 @@ Set Implicit Arguments.
 Unset Strict Implicit.
 Unset Printing Implicit Defensive.
 
+Set Warnings "-implicit-create-hint-db".
+
 (** **** Untyped Lambda Calculus *)
 
 Inductive term : Type :=
diff --git a/examples/ssr/SystemF_SN.v b/examples/ssr/SystemF_SN.v
index 9a58b02..df07039 100644
--- a/examples/ssr/SystemF_SN.v
+++ b/examples/ssr/SystemF_SN.v
@@ -8,6 +8,8 @@ Set Implicit Arguments.
 Unset Strict Implicit.
 Unset Printing Implicit Defensive.
 
+Set Warnings "-implicit-create-hint-db".
+
 (** **** Definitions *)
 
 Inductive type : Type :=
diff --git a/examples/ssr/pred_CC_omega.v b/examples/ssr/pred_CC_omega.v
index fa3cafb..1d2e48c 100644
--- a/examples/ssr/pred_CC_omega.v
+++ b/examples/ssr/pred_CC_omega.v
@@ -9,6 +9,8 @@ Set Implicit Arguments.
 Unset Strict Implicit.
 Unset Printing Implicit Defensive.
 
+Set Warnings "-implicit-create-hint-db".
+
 (** **** Curry-style type theory with a hierarchy of predicative universes. *)
 
 Inductive term : Type :=
diff --git a/theories/Autosubst_MMap.v b/theories/Autosubst_MMap.v
index c30c63c..2dbf246 100644
--- a/theories/Autosubst_MMap.v
+++ b/theories/Autosubst_MMap.v
@@ -10,6 +10,8 @@
 *)
 Require Import Autosubst_Basics.
 
+Set Warnings "-implicit-create-hint-db, -implicit-create-rewrite-hint-db".
+
 Class MMap (A B: Type) := mmap : (A -> A) -> B -> B.
 Arguments mmap {A B _} f !s /.
 

From fcc61ef019967f7af6ac457573c6c148cfe12837 Mon Sep 17 00:00:00 2001
From: skylee03 <i@skylee.xyz>
Date: Fri, 7 Aug 2026 22:01:22 +0800
Subject: [PATCH 15/24] unfix notation-for-abbreviation

---
 examples/ssr/BetaSubstitution.v | 4 ++--
 examples/ssr/CR.v               | 2 +-
 examples/ssr/SystemF_CBV.v      | 2 +-
 examples/ssr/SystemF_SN.v       | 2 +-
 examples/ssr/pred_CC_omega.v    | 2 +-
 5 files changed, 6 insertions(+), 6 deletions(-)

diff --git a/examples/ssr/BetaSubstitution.v b/examples/ssr/BetaSubstitution.v
index f0764ab..43188a7 100644
--- a/examples/ssr/BetaSubstitution.v
+++ b/examples/ssr/BetaSubstitution.v
@@ -25,7 +25,7 @@ Fixpoint lift_at (d k : nat) (s : term) : term :=
     | App s t => App (lift_at d k s) (lift_at d k t)
     | Lam s   => Lam (lift_at d.+1 k s)
   end.
-Abbreviation lift := (lift_at 0).
+Notation lift := (lift_at 0).
 
 Fixpoint sbst_at (d : nat) (t s : term) : term :=
   match s with
@@ -33,7 +33,7 @@ Fixpoint sbst_at (d : nat) (t s : term) : term :=
     | App s1 s2 => App (sbst_at d t s1) (sbst_at d t s2)
     | Lam s => Lam (sbst_at d.+1 t s)
   end.
-Abbreviation sbst := (sbst_at 0).
+Notation sbst := (sbst_at 0).
 
 (** Soundness proof *)
 
diff --git a/examples/ssr/CR.v b/examples/ssr/CR.v
index c9702af..83e7927 100644
--- a/examples/ssr/CR.v
+++ b/examples/ssr/CR.v
@@ -32,7 +32,7 @@ Inductive step : term -> term -> Prop :=
 | step_lam s1 s2 :
     step s1 s2 -> step (Lam s1) (Lam s2).
 
-Abbreviation red := (star step).
+Notation red := (star step).
 Notation "s === t" := (conv step s t) (at level 50).
 
 (*
diff --git a/examples/ssr/SystemF_CBV.v b/examples/ssr/SystemF_CBV.v
index 10f3500..c3dbea7 100644
--- a/examples/ssr/SystemF_CBV.v
+++ b/examples/ssr/SystemF_CBV.v
@@ -88,7 +88,7 @@ Fixpoint V (A : type) (rho : var -> term -> Prop) (v : term) {struct A} : Prop :
     | All A => exists2 s : term, v = TAbs s &
         forall i (B : type), L (V A (i .: rho)) s.|[B/]
   end.
-Abbreviation E A rho := (L (V A rho)).
+Notation E A rho := (L (V A rho)).
 
 Lemma V_value A rho v : V A rho v -> eval v v.
 Proof. by elim: A => [x[]|A _ B _/=[A'[s->]]|A _/=[s->]]. Qed.
diff --git a/examples/ssr/SystemF_SN.v b/examples/ssr/SystemF_SN.v
index df07039..a7e3ee1 100644
--- a/examples/ssr/SystemF_SN.v
+++ b/examples/ssr/SystemF_SN.v
@@ -153,7 +153,7 @@ Inductive has_type (Gamma : ctx) : term -> type -> Prop :=
 
 (* Strong Normalization *)
 
-Abbreviation sn := (sn step).
+Notation sn := (sn step).
 
 Lemma sn_closed t s : sn (App s t) -> sn s.
 Proof. apply: (sn_preimage (h := App^~t)) => x y. exact: step_appL. Qed.
diff --git a/examples/ssr/pred_CC_omega.v b/examples/ssr/pred_CC_omega.v
index 1d2e48c..bc37c7c 100644
--- a/examples/ssr/pred_CC_omega.v
+++ b/examples/ssr/pred_CC_omega.v
@@ -41,7 +41,7 @@ Inductive step : term -> term -> Prop :=
 | step_prodR A B1 B2 :
     step B1 B2 -> step (Prod A B1) (Prod A B2).
 
-Abbreviation red := (star step).
+Notation red := (star step).
 Notation "s === t" := (conv step s t) (at level 50).
 
 Definition sred sigma tau :=

From 7fca4e3dee1f66d706e281cf8776ba65a9b64b92 Mon Sep 17 00:00:00 2001
From: skylee03 <i@skylee.xyz>
Date: Fri, 7 Aug 2026 22:03:43 +0800
Subject: [PATCH 16/24] silence notation-for-abbreviation

---
 examples/ssr/BetaSubstitution.v | 2 ++
 examples/ssr/CR.v               | 2 +-
 examples/ssr/SystemF_CBV.v      | 2 ++
 examples/ssr/SystemF_SN.v       | 2 +-
 examples/ssr/pred_CC_omega.v    | 2 +-
 theories/Autosubst_Classes.v    | 4 +++-
 6 files changed, 10 insertions(+), 4 deletions(-)

diff --git a/examples/ssr/BetaSubstitution.v b/examples/ssr/BetaSubstitution.v
index 43188a7..40bbaac 100644
--- a/examples/ssr/BetaSubstitution.v
+++ b/examples/ssr/BetaSubstitution.v
@@ -5,6 +5,8 @@ Require Import Autosubst.
 Set Implicit Arguments.
 Unset Strict Implicit.
 
+Set Warnings "-notation-for-abbreviation".
+
 (** Untyped Lambda Terms and Parallel Substitutions *)
 
 Inductive term :=
diff --git a/examples/ssr/CR.v b/examples/ssr/CR.v
index 83e7927..4d1d354 100644
--- a/examples/ssr/CR.v
+++ b/examples/ssr/CR.v
@@ -6,7 +6,7 @@ Set Implicit Arguments.
 Unset Strict Implicit.
 Unset Printing Implicit Defensive.
 
-Set Warnings "-implicit-create-hint-db".
+Set Warnings "-implicit-create-hint-db, -notation-for-abbreviation".
 
 (** **** Untyped Lambda Calculus *)
 
diff --git a/examples/ssr/SystemF_CBV.v b/examples/ssr/SystemF_CBV.v
index c3dbea7..d47b9f5 100644
--- a/examples/ssr/SystemF_CBV.v
+++ b/examples/ssr/SystemF_CBV.v
@@ -7,6 +7,8 @@ Set Implicit Arguments.
 Unset Strict Implicit.
 Unset Printing Implicit Defensive.
 
+Set Warnings "-notation-for-abbreviation".
+
 (** **** Definitions *)
 
 Inductive type : Type :=
diff --git a/examples/ssr/SystemF_SN.v b/examples/ssr/SystemF_SN.v
index a7e3ee1..f54c1e4 100644
--- a/examples/ssr/SystemF_SN.v
+++ b/examples/ssr/SystemF_SN.v
@@ -8,7 +8,7 @@ Set Implicit Arguments.
 Unset Strict Implicit.
 Unset Printing Implicit Defensive.
 
-Set Warnings "-implicit-create-hint-db".
+Set Warnings "-implicit-create-hint-db, -notation-for-abbreviation".
 
 (** **** Definitions *)
 
diff --git a/examples/ssr/pred_CC_omega.v b/examples/ssr/pred_CC_omega.v
index bc37c7c..d5ffe5d 100644
--- a/examples/ssr/pred_CC_omega.v
+++ b/examples/ssr/pred_CC_omega.v
@@ -9,7 +9,7 @@ Set Implicit Arguments.
 Unset Strict Implicit.
 Unset Printing Implicit Defensive.
 
-Set Warnings "-implicit-create-hint-db".
+Set Warnings "-implicit-create-hint-db, -notation-for-abbreviation".
 
 (** **** Curry-style type theory with a hierarchy of predicative universes. *)
 
diff --git a/theories/Autosubst_Classes.v b/theories/Autosubst_Classes.v
index 279b199..14fa838 100644
--- a/theories/Autosubst_Classes.v
+++ b/theories/Autosubst_Classes.v
@@ -2,6 +2,8 @@
 (** Type classes and notations for substitutions. *)
 Require Import Autosubst_Basics Autosubst_MMap.
 
+Set Warnings "-notation-for-abbreviation".
+
 (**
   [_bind] is used to annotate the position of binders in inductive
   definitions of syntactic objects
@@ -114,7 +116,7 @@ Definition up {T} `{Ids T} `{Rename T} (sigma : var -> T) : var -> T :=
   ids 0 .: sigma >>> rename (+1).
 Arguments up {T _ _} sigma x : simpl never.
 
-Abbreviation upn := (iterate up).
+Notation upn := (iterate up).
 
 Definition upren (xi : var -> var) : (var -> var) := 0 .: xi >>> S.
 

From 0361b6bc36e0592adbcda4808908885a0b4750a2 Mon Sep 17 00:00:00 2001
From: skylee03 <i@skylee.xyz>
Date: Fri, 7 Aug 2026 22:20:09 +0800
Subject: [PATCH 17/24] fix postfix-notation-not-level-1

---
 theories/Autosubst_Classes.v | 24 ++++++++++++------------
 1 file changed, 12 insertions(+), 12 deletions(-)

diff --git a/theories/Autosubst_Classes.v b/theories/Autosubst_Classes.v
index 14fa838..95f6cc9 100644
--- a/theories/Autosubst_Classes.v
+++ b/theories/Autosubst_Classes.v
@@ -55,25 +55,25 @@ Notation "sigma >> tau" := (scomp sigma tau)
   (at level 56, left associativity) : subst_scope.
 
 Notation "s .[ sigma ]" := (subst sigma s)
-  (at level 2, sigma at level 200, left associativity,
+  (at level 1, sigma at level 200, left associativity,
    format "s .[ sigma ]" ) : subst_scope.
 Notation "s .[ t /]" := (subst (t .: ids) s)
-  (at level 2, t at level 200, left associativity,
+  (at level 1, t at level 200, left associativity,
    format "s .[ t /]") : subst_scope.
 Notation "s .[ t1 , t2 , .. , tn /]" :=
   (subst (scons t1 (scons t2 .. (scons tn ids) .. )) s)
-  (at level 2, left associativity,
+  (at level 1, left associativity,
    format "s '[ ' .[ t1 , '/' t2 , '/' .. , '/' tn /] ']'") : subst_scope.
 
 Notation "s ..[ sigma ]" := (mmap (subst sigma) s)
-  (at level 2, sigma at level 200, left associativity,
+  (at level 1, sigma at level 200, left associativity,
    format "s ..[ sigma ]" ) : subst_scope.
 Notation "s ..[ t /]" := (mmap (subst (t .: ids)) s)
-  (at level 2, t at level 200, left associativity,
+  (at level 1, t at level 200, left associativity,
    format "s ..[ t /]") : subst_scope.
 Notation "s ..[ t1 , t2 , .. , tn /]" :=
   (mmap (subst (scons t1 (scons t2 .. (scons tn ids) .. ))) s)
-  (at level 2, left associativity,
+  (at level 1, left associativity,
    format "s '[ ' ..[ t1 , '/' t2 , '/' .. , '/' tn /] ']'") : subst_scope.
 
 Definition hcomp {A B} `{HSubst A B} (f : var -> B) (g : var -> A) : var -> B
@@ -84,25 +84,25 @@ Notation "sigma >>| tau" := (hcomp sigma tau)
   (at level 56, left associativity) : subst_scope.
 
 Notation "s .|[ sigma ]" := (hsubst sigma s)
-  (at level 2, sigma at level 200, left associativity,
+  (at level 1, sigma at level 200, left associativity,
    format "s .|[ sigma ]" ) : subst_scope.
 Notation "s .|[ t /]" := (hsubst (t .: ids) s)
-  (at level 2, t at level 200, left associativity,
+  (at level 1, t at level 200, left associativity,
    format "s .|[ t /]") : subst_scope.
 Notation "s .|[ t1 , t2 , .. , tn /]" :=
   (hsubst (scons t1 (scons t2 .. (scons tn ids) .. )) s)
-  (at level 2, left associativity,
+  (at level 1, left associativity,
    format "s '[ ' .|[ t1 , '/' t2 , '/' .. , '/' tn /] ']'") : subst_scope.
 
 Notation "s ..|[ sigma ]" := (mmap (hsubst sigma) s)
-  (at level 2, sigma at level 200, left associativity,
+  (at level 1, sigma at level 200, left associativity,
    format "s ..|[ sigma ]" ) : subst_scope.
 Notation "s ..|[ t /]" := (mmap (hsubst (t .: ids)) s)
-  (at level 2, t at level 200, left associativity,
+  (at level 1, t at level 200, left associativity,
    format "s ..|[ t /]") : subst_scope.
 Notation "s ..|[ t1 , t2 , .. , tn /]" :=
   (mmap (hsubst (scons t1 (scons t2 .. (scons tn ids) .. ))) s)
-  (at level 2, left associativity,
+  (at level 1, left associativity,
    format "s '[ ' ..|[ t1 , '/' t2 , '/' .. , '/' tn /] ']'") : subst_scope.
 
 (** Coercion from renamings to substitutions. *)

From b3e629c7a58910de47948014b75605d2e065b54f Mon Sep 17 00:00:00 2001
From: Yang Ming-Tian <1178715749@qq.com>
Date: Fri, 7 Aug 2026 22:32:36 +0800
Subject: [PATCH 18/24] remove extra empty lines

Co-authored-by: Yang Ming-Tian <1178715749@qq.com>
---
 examples/plain/Size.v     | 1 -
 theories/Autosubst_MMap.v | 1 -
 2 files changed, 2 deletions(-)

diff --git a/examples/plain/Size.v b/examples/plain/Size.v
index b541b4f..af7fefc 100644
--- a/examples/plain/Size.v
+++ b/examples/plain/Size.v
@@ -95,7 +95,6 @@ Arguments size_fact {A} x {P _}.
 Lemma size_app (A : Type) (size_A : Size A) l1 l2 :
   size (app l1 l2) = size l1 + size l2.
 Proof. induction l1; simpl; intuition (auto with zarith). Qed.
-
 Global Hint Rewrite @size_app : size.
 
 Global Instance size_fact_app (A : Type) (size_A : Size A) l1 l2 :
diff --git a/theories/Autosubst_MMap.v b/theories/Autosubst_MMap.v
index 2dbf246..02820a3 100644
--- a/theories/Autosubst_MMap.v
+++ b/theories/Autosubst_MMap.v
@@ -146,7 +146,6 @@ Ltac derive_MMap :=
         let ys := tmap ys in exact ys
     end
   end.
-
 Global Hint Extern 0 (MMap _ _) => derive_MMap : derive.
 
 Ltac derive_MMapLemmas := constructor;

From 342463b3c48d0b01929f8b62d839251eadd64f08 Mon Sep 17 00:00:00 2001
From: skylee03 <i@skylee.xyz>
Date: Sat, 8 Aug 2026 01:05:24 +0800
Subject: [PATCH 19/24] unfix postfix-notation-not-level-1 and keep postfix
 notations at level 2

---
 theories/Autosubst_Classes.v | 24 ++++++++++++------------
 1 file changed, 12 insertions(+), 12 deletions(-)

diff --git a/theories/Autosubst_Classes.v b/theories/Autosubst_Classes.v
index 95f6cc9..14fa838 100644
--- a/theories/Autosubst_Classes.v
+++ b/theories/Autosubst_Classes.v
@@ -55,25 +55,25 @@ Notation "sigma >> tau" := (scomp sigma tau)
   (at level 56, left associativity) : subst_scope.
 
 Notation "s .[ sigma ]" := (subst sigma s)
-  (at level 1, sigma at level 200, left associativity,
+  (at level 2, sigma at level 200, left associativity,
    format "s .[ sigma ]" ) : subst_scope.
 Notation "s .[ t /]" := (subst (t .: ids) s)
-  (at level 1, t at level 200, left associativity,
+  (at level 2, t at level 200, left associativity,
    format "s .[ t /]") : subst_scope.
 Notation "s .[ t1 , t2 , .. , tn /]" :=
   (subst (scons t1 (scons t2 .. (scons tn ids) .. )) s)
-  (at level 1, left associativity,
+  (at level 2, left associativity,
    format "s '[ ' .[ t1 , '/' t2 , '/' .. , '/' tn /] ']'") : subst_scope.
 
 Notation "s ..[ sigma ]" := (mmap (subst sigma) s)
-  (at level 1, sigma at level 200, left associativity,
+  (at level 2, sigma at level 200, left associativity,
    format "s ..[ sigma ]" ) : subst_scope.
 Notation "s ..[ t /]" := (mmap (subst (t .: ids)) s)
-  (at level 1, t at level 200, left associativity,
+  (at level 2, t at level 200, left associativity,
    format "s ..[ t /]") : subst_scope.
 Notation "s ..[ t1 , t2 , .. , tn /]" :=
   (mmap (subst (scons t1 (scons t2 .. (scons tn ids) .. ))) s)
-  (at level 1, left associativity,
+  (at level 2, left associativity,
    format "s '[ ' ..[ t1 , '/' t2 , '/' .. , '/' tn /] ']'") : subst_scope.
 
 Definition hcomp {A B} `{HSubst A B} (f : var -> B) (g : var -> A) : var -> B
@@ -84,25 +84,25 @@ Notation "sigma >>| tau" := (hcomp sigma tau)
   (at level 56, left associativity) : subst_scope.
 
 Notation "s .|[ sigma ]" := (hsubst sigma s)
-  (at level 1, sigma at level 200, left associativity,
+  (at level 2, sigma at level 200, left associativity,
    format "s .|[ sigma ]" ) : subst_scope.
 Notation "s .|[ t /]" := (hsubst (t .: ids) s)
-  (at level 1, t at level 200, left associativity,
+  (at level 2, t at level 200, left associativity,
    format "s .|[ t /]") : subst_scope.
 Notation "s .|[ t1 , t2 , .. , tn /]" :=
   (hsubst (scons t1 (scons t2 .. (scons tn ids) .. )) s)
-  (at level 1, left associativity,
+  (at level 2, left associativity,
    format "s '[ ' .|[ t1 , '/' t2 , '/' .. , '/' tn /] ']'") : subst_scope.
 
 Notation "s ..|[ sigma ]" := (mmap (hsubst sigma) s)
-  (at level 1, sigma at level 200, left associativity,
+  (at level 2, sigma at level 200, left associativity,
    format "s ..|[ sigma ]" ) : subst_scope.
 Notation "s ..|[ t /]" := (mmap (hsubst (t .: ids)) s)
-  (at level 1, t at level 200, left associativity,
+  (at level 2, t at level 200, left associativity,
    format "s ..|[ t /]") : subst_scope.
 Notation "s ..|[ t1 , t2 , .. , tn /]" :=
   (mmap (hsubst (scons t1 (scons t2 .. (scons tn ids) .. ))) s)
-  (at level 1, left associativity,
+  (at level 2, left associativity,
    format "s '[ ' ..|[ t1 , '/' t2 , '/' .. , '/' tn /] ']'") : subst_scope.
 
 (** Coercion from renamings to substitutions. *)

From a1f123466463e11b4fadcd5caae8e70313ded3f8 Mon Sep 17 00:00:00 2001
From: skylee03 <i@skylee.xyz>
Date: Sat, 8 Aug 2026 09:37:40 +0800
Subject: [PATCH 20/24] make `Set Warnings` local

---
 examples/plain/Size.v           | 2 +-
 examples/ssr/BetaSubstitution.v | 2 +-
 examples/ssr/CR.v               | 2 +-
 examples/ssr/SystemF_CBV.v      | 2 +-
 examples/ssr/SystemF_SN.v       | 2 +-
 examples/ssr/pred_CC_omega.v    | 2 +-
 theories/Autosubst_Classes.v    | 2 +-
 theories/Autosubst_MMap.v       | 2 +-
 8 files changed, 8 insertions(+), 8 deletions(-)

diff --git a/examples/plain/Size.v b/examples/plain/Size.v
index af7fefc..1542878 100644
--- a/examples/plain/Size.v
+++ b/examples/plain/Size.v
@@ -2,7 +2,7 @@
 From Stdlib Require Import ZArith Lia List Program.Equality.
 Require Import Autosubst.Autosubst_Basics.
 
-Set Warnings "-implicit-create-hint-db, -implicit-create-rewrite-hint-db".
+Local Set Warnings "-implicit-create-hint-db, -implicit-create-rewrite-hint-db".
 
 Class Size (A : Type) := size : A -> nat.
 
diff --git a/examples/ssr/BetaSubstitution.v b/examples/ssr/BetaSubstitution.v
index 40bbaac..90eb204 100644
--- a/examples/ssr/BetaSubstitution.v
+++ b/examples/ssr/BetaSubstitution.v
@@ -5,7 +5,7 @@ Require Import Autosubst.
 Set Implicit Arguments.
 Unset Strict Implicit.
 
-Set Warnings "-notation-for-abbreviation".
+Local Set Warnings "-notation-for-abbreviation".
 
 (** Untyped Lambda Terms and Parallel Substitutions *)
 
diff --git a/examples/ssr/CR.v b/examples/ssr/CR.v
index 4d1d354..5348e5e 100644
--- a/examples/ssr/CR.v
+++ b/examples/ssr/CR.v
@@ -6,7 +6,7 @@ Set Implicit Arguments.
 Unset Strict Implicit.
 Unset Printing Implicit Defensive.
 
-Set Warnings "-implicit-create-hint-db, -notation-for-abbreviation".
+Local Set Warnings "-implicit-create-hint-db, -notation-for-abbreviation".
 
 (** **** Untyped Lambda Calculus *)
 
diff --git a/examples/ssr/SystemF_CBV.v b/examples/ssr/SystemF_CBV.v
index d47b9f5..86dd0aa 100644
--- a/examples/ssr/SystemF_CBV.v
+++ b/examples/ssr/SystemF_CBV.v
@@ -7,7 +7,7 @@ Set Implicit Arguments.
 Unset Strict Implicit.
 Unset Printing Implicit Defensive.
 
-Set Warnings "-notation-for-abbreviation".
+Local Set Warnings "-notation-for-abbreviation".
 
 (** **** Definitions *)
 
diff --git a/examples/ssr/SystemF_SN.v b/examples/ssr/SystemF_SN.v
index f54c1e4..83187fb 100644
--- a/examples/ssr/SystemF_SN.v
+++ b/examples/ssr/SystemF_SN.v
@@ -8,7 +8,7 @@ Set Implicit Arguments.
 Unset Strict Implicit.
 Unset Printing Implicit Defensive.
 
-Set Warnings "-implicit-create-hint-db, -notation-for-abbreviation".
+Local Set Warnings "-implicit-create-hint-db, -notation-for-abbreviation".
 
 (** **** Definitions *)
 
diff --git a/examples/ssr/pred_CC_omega.v b/examples/ssr/pred_CC_omega.v
index d5ffe5d..cc38e93 100644
--- a/examples/ssr/pred_CC_omega.v
+++ b/examples/ssr/pred_CC_omega.v
@@ -9,7 +9,7 @@ Set Implicit Arguments.
 Unset Strict Implicit.
 Unset Printing Implicit Defensive.
 
-Set Warnings "-implicit-create-hint-db, -notation-for-abbreviation".
+Local Set Warnings "-implicit-create-hint-db, -notation-for-abbreviation".
 
 (** **** Curry-style type theory with a hierarchy of predicative universes. *)
 
diff --git a/theories/Autosubst_Classes.v b/theories/Autosubst_Classes.v
index 14fa838..af2771e 100644
--- a/theories/Autosubst_Classes.v
+++ b/theories/Autosubst_Classes.v
@@ -2,7 +2,7 @@
 (** Type classes and notations for substitutions. *)
 Require Import Autosubst_Basics Autosubst_MMap.
 
-Set Warnings "-notation-for-abbreviation".
+Local Set Warnings "-notation-for-abbreviation".
 
 (**
   [_bind] is used to annotate the position of binders in inductive
diff --git a/theories/Autosubst_MMap.v b/theories/Autosubst_MMap.v
index 02820a3..c664f9e 100644
--- a/theories/Autosubst_MMap.v
+++ b/theories/Autosubst_MMap.v
@@ -10,7 +10,7 @@
 *)
 Require Import Autosubst_Basics.
 
-Set Warnings "-implicit-create-hint-db, -implicit-create-rewrite-hint-db".
+Local Set Warnings "-implicit-create-hint-db, -implicit-create-rewrite-hint-db".
 
 Class MMap (A B: Type) := mmap : (A -> A) -> B -> B.
 Arguments mmap {A B _} f !s /.

From 2863f2bfac2bd445270c583ea7ef205091385bea Mon Sep 17 00:00:00 2001
From: skylee03 <i@skylee.xyz>
Date: Sat, 8 Aug 2026 09:49:23 +0800
Subject: [PATCH 21/24] add comments to `Set Warnings`

---
 examples/plain/Size.v           | 1 +
 examples/ssr/BetaSubstitution.v | 1 +
 examples/ssr/CR.v               | 1 +
 examples/ssr/SystemF_CBV.v      | 1 +
 examples/ssr/SystemF_SN.v       | 1 +
 examples/ssr/pred_CC_omega.v    | 1 +
 theories/Autosubst_Classes.v    | 1 +
 theories/Autosubst_MMap.v       | 1 +
 8 files changed, 8 insertions(+)

diff --git a/examples/plain/Size.v b/examples/plain/Size.v
index 1542878..7ed682b 100644
--- a/examples/plain/Size.v
+++ b/examples/plain/Size.v
@@ -2,6 +2,7 @@
 From Stdlib Require Import ZArith Lia List Program.Equality.
 Require Import Autosubst.Autosubst_Basics.
 
+(* Silence Rocq 9.2 deprecation warnings *)
 Local Set Warnings "-implicit-create-hint-db, -implicit-create-rewrite-hint-db".
 
 Class Size (A : Type) := size : A -> nat.
diff --git a/examples/ssr/BetaSubstitution.v b/examples/ssr/BetaSubstitution.v
index 90eb204..95c2a6d 100644
--- a/examples/ssr/BetaSubstitution.v
+++ b/examples/ssr/BetaSubstitution.v
@@ -5,6 +5,7 @@ Require Import Autosubst.
 Set Implicit Arguments.
 Unset Strict Implicit.
 
+(* Silence Rocq 9.2 deprecation warnings *)
 Local Set Warnings "-notation-for-abbreviation".
 
 (** Untyped Lambda Terms and Parallel Substitutions *)
diff --git a/examples/ssr/CR.v b/examples/ssr/CR.v
index 5348e5e..36ea90c 100644
--- a/examples/ssr/CR.v
+++ b/examples/ssr/CR.v
@@ -6,6 +6,7 @@ Set Implicit Arguments.
 Unset Strict Implicit.
 Unset Printing Implicit Defensive.
 
+(* Silence Rocq 9.2 deprecation warnings *)
 Local Set Warnings "-implicit-create-hint-db, -notation-for-abbreviation".
 
 (** **** Untyped Lambda Calculus *)
diff --git a/examples/ssr/SystemF_CBV.v b/examples/ssr/SystemF_CBV.v
index 86dd0aa..2cb0e98 100644
--- a/examples/ssr/SystemF_CBV.v
+++ b/examples/ssr/SystemF_CBV.v
@@ -7,6 +7,7 @@ Set Implicit Arguments.
 Unset Strict Implicit.
 Unset Printing Implicit Defensive.
 
+(* Silence Rocq 9.2 deprecation warnings *)
 Local Set Warnings "-notation-for-abbreviation".
 
 (** **** Definitions *)
diff --git a/examples/ssr/SystemF_SN.v b/examples/ssr/SystemF_SN.v
index 83187fb..54a0c0a 100644
--- a/examples/ssr/SystemF_SN.v
+++ b/examples/ssr/SystemF_SN.v
@@ -8,6 +8,7 @@ Set Implicit Arguments.
 Unset Strict Implicit.
 Unset Printing Implicit Defensive.
 
+(* Silence Rocq 9.2 deprecation warnings *)
 Local Set Warnings "-implicit-create-hint-db, -notation-for-abbreviation".
 
 (** **** Definitions *)
diff --git a/examples/ssr/pred_CC_omega.v b/examples/ssr/pred_CC_omega.v
index cc38e93..2534e5e 100644
--- a/examples/ssr/pred_CC_omega.v
+++ b/examples/ssr/pred_CC_omega.v
@@ -9,6 +9,7 @@ Set Implicit Arguments.
 Unset Strict Implicit.
 Unset Printing Implicit Defensive.
 
+(* Silence Rocq 9.2 deprecation warnings *)
 Local Set Warnings "-implicit-create-hint-db, -notation-for-abbreviation".
 
 (** **** Curry-style type theory with a hierarchy of predicative universes. *)
diff --git a/theories/Autosubst_Classes.v b/theories/Autosubst_Classes.v
index af2771e..1ecda2a 100644
--- a/theories/Autosubst_Classes.v
+++ b/theories/Autosubst_Classes.v
@@ -2,6 +2,7 @@
 (** Type classes and notations for substitutions. *)
 Require Import Autosubst_Basics Autosubst_MMap.
 
+(* Silence Rocq 9.2 deprecation warnings *)
 Local Set Warnings "-notation-for-abbreviation".
 
 (**
diff --git a/theories/Autosubst_MMap.v b/theories/Autosubst_MMap.v
index c664f9e..73d50c6 100644
--- a/theories/Autosubst_MMap.v
+++ b/theories/Autosubst_MMap.v
@@ -10,6 +10,7 @@
 *)
 Require Import Autosubst_Basics.
 
+(* Silence Rocq 9.2 deprecation warnings *)
 Local Set Warnings "-implicit-create-hint-db, -implicit-create-rewrite-hint-db".
 
 Class MMap (A B: Type) := mmap : (A -> A) -> B -> B.

From c804a791290830bf4773196ec3bba051485eab47 Mon Sep 17 00:00:00 2001
From: skylee03 <i@skylee.xyz>
Date: Sat, 8 Aug 2026 09:54:12 +0800
Subject: [PATCH 22/24] fix postfix-notation-not-level-1

---
 theories/Autosubst_Classes.v | 12 ++++++++++++
 1 file changed, 12 insertions(+)

diff --git a/theories/Autosubst_Classes.v b/theories/Autosubst_Classes.v
index 1ecda2a..ae0a094 100644
--- a/theories/Autosubst_Classes.v
+++ b/theories/Autosubst_Classes.v
@@ -55,23 +55,29 @@ Arguments scomp {A _} f g x /.
 Notation "sigma >> tau" := (scomp sigma tau)
   (at level 56, left associativity) : subst_scope.
 
+#[warnings="-postfix-notation-not-level-1"]
 Notation "s .[ sigma ]" := (subst sigma s)
   (at level 2, sigma at level 200, left associativity,
    format "s .[ sigma ]" ) : subst_scope.
+#[warnings="-postfix-notation-not-level-1"]
 Notation "s .[ t /]" := (subst (t .: ids) s)
   (at level 2, t at level 200, left associativity,
    format "s .[ t /]") : subst_scope.
+#[warnings="-postfix-notation-not-level-1"]
 Notation "s .[ t1 , t2 , .. , tn /]" :=
   (subst (scons t1 (scons t2 .. (scons tn ids) .. )) s)
   (at level 2, left associativity,
    format "s '[ ' .[ t1 , '/' t2 , '/' .. , '/' tn /] ']'") : subst_scope.
 
+#[warnings="-postfix-notation-not-level-1"]
 Notation "s ..[ sigma ]" := (mmap (subst sigma) s)
   (at level 2, sigma at level 200, left associativity,
    format "s ..[ sigma ]" ) : subst_scope.
+#[warnings="-postfix-notation-not-level-1"]
 Notation "s ..[ t /]" := (mmap (subst (t .: ids)) s)
   (at level 2, t at level 200, left associativity,
    format "s ..[ t /]") : subst_scope.
+#[warnings="-postfix-notation-not-level-1"]
 Notation "s ..[ t1 , t2 , .. , tn /]" :=
   (mmap (subst (scons t1 (scons t2 .. (scons tn ids) .. ))) s)
   (at level 2, left associativity,
@@ -84,23 +90,29 @@ Arguments hcomp {A B _} f g x /.
 Notation "sigma >>| tau" := (hcomp sigma tau)
   (at level 56, left associativity) : subst_scope.
 
+#[warnings="-postfix-notation-not-level-1"]
 Notation "s .|[ sigma ]" := (hsubst sigma s)
   (at level 2, sigma at level 200, left associativity,
    format "s .|[ sigma ]" ) : subst_scope.
+#[warnings="-postfix-notation-not-level-1"]
 Notation "s .|[ t /]" := (hsubst (t .: ids) s)
   (at level 2, t at level 200, left associativity,
    format "s .|[ t /]") : subst_scope.
+#[warnings="-postfix-notation-not-level-1"]
 Notation "s .|[ t1 , t2 , .. , tn /]" :=
   (hsubst (scons t1 (scons t2 .. (scons tn ids) .. )) s)
   (at level 2, left associativity,
    format "s '[ ' .|[ t1 , '/' t2 , '/' .. , '/' tn /] ']'") : subst_scope.
 
+#[warnings="-postfix-notation-not-level-1"]
 Notation "s ..|[ sigma ]" := (mmap (hsubst sigma) s)
   (at level 2, sigma at level 200, left associativity,
    format "s ..|[ sigma ]" ) : subst_scope.
+#[warnings="-postfix-notation-not-level-1"]
 Notation "s ..|[ t /]" := (mmap (hsubst (t .: ids)) s)
   (at level 2, t at level 200, left associativity,
    format "s ..|[ t /]") : subst_scope.
+#[warnings="-postfix-notation-not-level-1"]
 Notation "s ..|[ t1 , t2 , .. , tn /]" :=
   (mmap (hsubst (scons t1 (scons t2 .. (scons tn ids) .. ))) s)
   (at level 2, left associativity,

From 1d38f4591cbc04bf0aa8936b7562df599bf5930d Mon Sep 17 00:00:00 2001
From: skylee03 <i@skylee.xyz>
Date: Sat, 8 Aug 2026 17:57:33 +0800
Subject: [PATCH 23/24] make `-postfix-notation-not-level-1` file level

---
 theories/Autosubst_Classes.v | 15 +++------------
 1 file changed, 3 insertions(+), 12 deletions(-)

diff --git a/theories/Autosubst_Classes.v b/theories/Autosubst_Classes.v
index ae0a094..a3ca9f7 100644
--- a/theories/Autosubst_Classes.v
+++ b/theories/Autosubst_Classes.v
@@ -5,6 +5,9 @@ Require Import Autosubst_Basics Autosubst_MMap.
 (* Silence Rocq 9.2 deprecation warnings *)
 Local Set Warnings "-notation-for-abbreviation".
 
+(* Silence postfix notation level warnings *)
+Local Set Warnings "-postfix-notation-not-level-1".
+
 (**
   [_bind] is used to annotate the position of binders in inductive
   definitions of syntactic objects
@@ -55,29 +58,23 @@ Arguments scomp {A _} f g x /.
 Notation "sigma >> tau" := (scomp sigma tau)
   (at level 56, left associativity) : subst_scope.
 
-#[warnings="-postfix-notation-not-level-1"]
 Notation "s .[ sigma ]" := (subst sigma s)
   (at level 2, sigma at level 200, left associativity,
    format "s .[ sigma ]" ) : subst_scope.
-#[warnings="-postfix-notation-not-level-1"]
 Notation "s .[ t /]" := (subst (t .: ids) s)
   (at level 2, t at level 200, left associativity,
    format "s .[ t /]") : subst_scope.
-#[warnings="-postfix-notation-not-level-1"]
 Notation "s .[ t1 , t2 , .. , tn /]" :=
   (subst (scons t1 (scons t2 .. (scons tn ids) .. )) s)
   (at level 2, left associativity,
    format "s '[ ' .[ t1 , '/' t2 , '/' .. , '/' tn /] ']'") : subst_scope.
 
-#[warnings="-postfix-notation-not-level-1"]
 Notation "s ..[ sigma ]" := (mmap (subst sigma) s)
   (at level 2, sigma at level 200, left associativity,
    format "s ..[ sigma ]" ) : subst_scope.
-#[warnings="-postfix-notation-not-level-1"]
 Notation "s ..[ t /]" := (mmap (subst (t .: ids)) s)
   (at level 2, t at level 200, left associativity,
    format "s ..[ t /]") : subst_scope.
-#[warnings="-postfix-notation-not-level-1"]
 Notation "s ..[ t1 , t2 , .. , tn /]" :=
   (mmap (subst (scons t1 (scons t2 .. (scons tn ids) .. ))) s)
   (at level 2, left associativity,
@@ -90,29 +87,23 @@ Arguments hcomp {A B _} f g x /.
 Notation "sigma >>| tau" := (hcomp sigma tau)
   (at level 56, left associativity) : subst_scope.
 
-#[warnings="-postfix-notation-not-level-1"]
 Notation "s .|[ sigma ]" := (hsubst sigma s)
   (at level 2, sigma at level 200, left associativity,
    format "s .|[ sigma ]" ) : subst_scope.
-#[warnings="-postfix-notation-not-level-1"]
 Notation "s .|[ t /]" := (hsubst (t .: ids) s)
   (at level 2, t at level 200, left associativity,
    format "s .|[ t /]") : subst_scope.
-#[warnings="-postfix-notation-not-level-1"]
 Notation "s .|[ t1 , t2 , .. , tn /]" :=
   (hsubst (scons t1 (scons t2 .. (scons tn ids) .. )) s)
   (at level 2, left associativity,
    format "s '[ ' .|[ t1 , '/' t2 , '/' .. , '/' tn /] ']'") : subst_scope.
 
-#[warnings="-postfix-notation-not-level-1"]
 Notation "s ..|[ sigma ]" := (mmap (hsubst sigma) s)
   (at level 2, sigma at level 200, left associativity,
    format "s ..|[ sigma ]" ) : subst_scope.
-#[warnings="-postfix-notation-not-level-1"]
 Notation "s ..|[ t /]" := (mmap (hsubst (t .: ids)) s)
   (at level 2, t at level 200, left associativity,
    format "s ..|[ t /]") : subst_scope.
-#[warnings="-postfix-notation-not-level-1"]
 Notation "s ..|[ t1 , t2 , .. , tn /]" :=
   (mmap (hsubst (scons t1 (scons t2 .. (scons tn ids) .. ))) s)
   (at level 2, left associativity,

From eb57d3a7a0f5d328aded946372e72985cac59b32 Mon Sep 17 00:00:00 2001
From: Yang Ming-Tian <1178715749@qq.com>
Date: Sat, 8 Aug 2026 18:04:39 +0800
Subject: [PATCH 24/24] update `-postfix-notation-not-level-1` comment

Co-authored-by: Ralf Jung <post@ralfj.de>
---
 theories/Autosubst_Classes.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/theories/Autosubst_Classes.v b/theories/Autosubst_Classes.v
index a3ca9f7..5b55ff5 100644
--- a/theories/Autosubst_Classes.v
+++ b/theories/Autosubst_Classes.v
@@ -5,7 +5,7 @@ Require Import Autosubst_Basics Autosubst_MMap.
 (* Silence Rocq 9.2 deprecation warnings *)
 Local Set Warnings "-notation-for-abbreviation".
 
-(* Silence postfix notation level warnings *)
+(* Silence postfix notation level warnings: we don't want to risk changing the levels. *)
 Local Set Warnings "-postfix-notation-not-level-1".
 
 (**