Fix warnings for Rocq

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) :=

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.

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.

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 /.

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.

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 :=

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 :

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:

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 :=