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..a9ee8ff 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 Stdlib Require Import Program.Equality List Lia.
 Require Import Autosubst.Autosubst.
 Require Import Size Decidable Context.
 
@@ -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.
diff --git a/examples/plain/Size.v b/examples/plain/Size.v
index 0a8669b..7ed682b 100644
--- a/examples/plain/Size.v
+++ b/examples/plain/Size.v
@@ -1,7 +1,10 @@
 (** * 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.
 
+(* 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.
 
 Arguments size {A _} !x /.
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/BetaSubstitution.v b/examples/ssr/BetaSubstitution.v
index 43188a7..95c2a6d 100644
--- a/examples/ssr/BetaSubstitution.v
+++ b/examples/ssr/BetaSubstitution.v
@@ -5,6 +5,9 @@ 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 *)
 
 Inductive term :=
diff --git a/examples/ssr/CR.v b/examples/ssr/CR.v
index d6cbd27..36ea90c 100644
--- a/examples/ssr/CR.v
+++ b/examples/ssr/CR.v
@@ -1,11 +1,14 @@
 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.
 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 *)
 
 Inductive term : Type :=
@@ -94,16 +97,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} //=; 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 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 => /=; auto using pstep. move=> s1 s2 t1 t2 _ A _ B sigma.
+  eapply pstep_ebeta => //. by autosubst.
 Qed.
 
 Lemma psstep_up sigma tau :
@@ -114,10 +117,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; auto 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; auto using psstep_up.
 Qed.
 
 Lemma pstep_compat_beta s1 s2 t1 t2 :
@@ -127,11 +130,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} //=; 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 => //=...
-    move=> s A ih1. inv A. inv ih1...
+  - 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 e716fca..ac37248 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} /=; 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.
@@ -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}; auto using sub. move=> Gamma A C h1 h2. inv h2; auto 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; auto 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; 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. eapply ih2; eauto. move: H3. apply: sub_narrow_t; auto using sub.
     + case=> //= _. exact: sub_weak.
-    + move=> [|x] _... right => /=. asimpl. exact: transitivity_ren.
+    + move=> [|x] _; auto. 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; auto.
     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.
   - 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_CBV.v b/examples/ssr/SystemF_CBV.v
index c3dbea7..2cb0e98 100644
--- a/examples/ssr/SystemF_CBV.v
+++ b/examples/ssr/SystemF_CBV.v
@@ -7,6 +7,9 @@ Set Implicit Arguments.
 Unset Strict Implicit.
 Unset Printing Implicit Defensive.
 
+(* Silence Rocq 9.2 deprecation warnings *)
+Local Set Warnings "-notation-for-abbreviation".
+
 (** **** Definitions *)
 
 Inductive type : Type :=
diff --git a/examples/ssr/SystemF_SN.v b/examples/ssr/SystemF_SN.v
index 5c55abf..54a0c0a 100644
--- a/examples/ssr/SystemF_SN.v
+++ b/examples/ssr/SystemF_SN.v
@@ -1,13 +1,16 @@
 (** * 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.
 Unset Strict Implicit.
 Unset Printing Implicit Defensive.
 
+(* Silence Rocq 9.2 deprecation warnings *)
+Local Set Warnings "-implicit-create-hint-db, -notation-for-abbreviation".
+
 (** **** Definitions *)
 
 Inductive type : Type :=
@@ -209,22 +212,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; auto.
   - 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)); auto.
       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)); auto 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; 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...
-    + move=> s t h st P B rep. apply: p_cl (step_tapp B st)...
       by apply/ih/ad_cons.
-    + move=> s ns h P B rep. apply ih... exact: ad_cons.
-      move=> t st. inv st => //...
+    + 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.
@@ -249,7 +252,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 +289,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 +315,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 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 fae03f0..2534e5e 100644
--- a/examples/ssr/pred_CC_omega.v
+++ b/examples/ssr/pred_CC_omega.v
@@ -2,13 +2,16 @@
  *)
 
 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.
 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. *)
 
 Inductive term : Type :=
@@ -180,10 +183,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 psstep_up.
 Qed.
 
 Lemma pstep_compat_beta s1 s2 t1 t2 :
@@ -193,11 +196,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 +274,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 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...
+  - 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... eapply conv_prod... exact: conv_prod.
+      eapply SubI. eapply sub1_prod; eauto. eapply conv_prod => //. exact: conv_prod.
 Qed.
 
 Lemma sub_trans B A C :
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.
diff --git a/theories/Autosubst_Classes.v b/theories/Autosubst_Classes.v
index b3f608c..5b55ff5 100644
--- a/theories/Autosubst_Classes.v
+++ b/theories/Autosubst_Classes.v
@@ -2,6 +2,12 @@
 (** Type classes and notations for substitutions. *)
 Require Import Autosubst_Basics Autosubst_MMap.
 
+(* Silence Rocq 9.2 deprecation warnings *)
+Local Set Warnings "-notation-for-abbreviation".
+
+(* Silence postfix notation level warnings: we don't want to risk changing the levels. *)
+Local Set Warnings "-postfix-notation-not-level-1".
+
 (**
   [_bind] is used to annotate the position of binders in inductive
   definitions of syntactic objects
diff --git a/theories/Autosubst_MMap.v b/theories/Autosubst_MMap.v
index 5d75b28..73d50c6 100644
--- a/theories/Autosubst_MMap.v
+++ b/theories/Autosubst_MMap.v
@@ -10,6 +10,9 @@
 *)
 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.
 Arguments mmap {A B _} f !s /.
 
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.