Fix deprecations on 8.19 and 8.20, update CI

.github/workflows/docker-action.yml

@@ -18,6 +18,8 @@ jobs:
       matrix:
         image:
           - 'mathcomp/mathcomp-dev:coq-dev'
+          - 'mathcomp/mathcomp:2.2.0-coq-8.19'
+          - 'mathcomp/mathcomp:2.1.0-coq-8.18'
           - 'mathcomp/mathcomp:2.0.0-coq-8.17'
           - 'mathcomp/mathcomp:1.17.0-coq-8.17'
           - 'mathcomp/mathcomp:1.16.0-coq-8.17'

coq-autosubst.opam

@@ -23,7 +23,7 @@ substitutions."""
 build: [make "-j%{jobs}%"]
 install: [make "install"]
 depends: [
-  "coq" {(>= "8.14" & < "8.18~") | (= "dev")}
+  "coq" {(>= "8.14" & < "8.21~") | (= "dev")}
 ]
 
 tags: [

examples/plain/Context.v

@@ -67,12 +67,13 @@ Proof.
   - split.
     + autosubst.
     + autosubst.
-  - simpl. cutrewrite (A.[ren (+S (length Delta))] =
-                       A.[ren(+length Delta)].[ren(+1)]); [idtac|autosubst].
+  - simpl.
+    replace (A.[ren (+S (length Delta))]) with
+      (A.[ren(+length Delta)].[ren(+1)]); [idtac|autosubst].
     split.
-      + econstructor. eapply IHDelta; eassumption. reflexivity.
-      + intros H. inv H. rewrite IHDelta. apply lift_inj in H5.
-        subst. eassumption.
+    + econstructor. eapply IHDelta; eassumption. reflexivity.
+    + intros H. inv H. rewrite IHDelta. apply lift_inj in H5.
+      subst. eassumption.
 Qed.
 
 Lemma atnd_steps' x Gamma Delta A :
@@ -83,7 +84,7 @@ Proof.
   induction Delta; intros.
   - exists A.
     simpl in H.
-    rewrite plus_0_r in H. intuition autosubst.
+    rewrite Nat.add_0_r in H. intuition autosubst.
   - asimpl. simpl in *.
     rewrite plusnS in *.
     inv H.

examples/plain/POPLmark.v

@@ -192,7 +192,7 @@ Proof.
         * now rewrite ren_size_inv.
         * intros. change (B' :: Delta) with ((B' :: nil) ++ Delta).
           rewrite app_assoc.
-          cutrewrite (S (length Delta') = length (Delta' ++ B' :: nil)).
+          replace (S (length Delta')) with (length (Delta' ++ B' :: nil)).
           now apply atnd_steps.
           rewrite app_length. simpl. lia.
         * asimpl in IHsub.
@@ -298,7 +298,8 @@ Lemma ty_weak_ty  xi Delta1 Delta2 Gamma1 Gamma2 s s' A A':
   s' = s.|[ren xi] ->
   TY Delta2;Gamma2 |- s' : A'.
 Proof.
-  intros. subst. cutrewrite(s.|[ren xi] = s.|[ren xi].[ren id]).
+  intros. subst.
+  replace (s.|[ren xi]) with (s.|[ren xi].[ren id]).
   eapply ty_weak; eauto. now autosubst.
 Qed.
 
@@ -319,8 +320,8 @@ Lemma ty_weak_ter xi Delta Gamma1 Gamma2 s A :
   TY Delta;Gamma2 |- s.[ren xi] : A.
 Proof.
   intros.
-  cutrewrite (s = s.|[ren id]).
-  cutrewrite (A = A.[ren id]).
+  replace s with (s.|[ren id]).
+  replace A with (A.[ren id]).
   eapply ty_weak; eauto; intros; asimpl; now eauto.
   autosubst. autosubst.
 Qed.
@@ -415,8 +416,8 @@ Corollary ty_subst_term Delta Gamma1 Gamma2 s A sigma:
   TY Delta;Gamma2 |- s.[sigma] : A.
 Proof.
   intros.
-  cutrewrite(s = s.|[ids]);[idtac|autosubst].
-  cutrewrite (A = A.[ids]);[idtac|autosubst].
+  replace s with (s.|[ids]);[idtac|autosubst].
+  replace A with (A.[ids]);[idtac|autosubst].
   eapply ty_subst; eauto; intros.
   - asimpl; eauto using sub, sub_refl.
   - asimpl; eauto using sub, sub_refl.
@@ -488,7 +489,7 @@ Proof.
     + pose proof (ty_inv_abs H0 H1) as [? [B' [? ?]]].
       eapply ty_subst_term; eauto using ty.
       intros [|] ? ?; simpl in *; subst; eauto using ty.
-  - cutrewrite (s.|[B/] = s.|[B/].[ids]);[idtac|autosubst].
+  - replace (s.|[B/]) with (s.|[B/].[ids]);[idtac|autosubst].
     inv H_ty; [idtac | pose proof (ty_inv_tabs H1 H2) as [? [B' [? ?]]]];
     (eapply ty_subst; eauto using ty; [
         now intros ? ? H_atnd; inv H_atnd; asimpl; eauto using sub, sub_refl

examples/plain/Size.v

@@ -92,7 +92,7 @@ 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. Qed.
+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 :

examples/ssr/ARS.v

@@ -7,6 +7,7 @@ Set Implicit Arguments.
 Unset Strict Implicit.
 Unset Printing Implicit Defensive.
 
+Declare Scope prop_scope.
 Delimit Scope prop_scope with PROP.
 Open Scope prop_scope.
 
@@ -41,7 +42,7 @@ Definition diamond := forall x y z, e x y -> e x z -> exists2 u, e y u & e z u.
 Definition confluent := forall x y z, star x y -> star x z -> joinable star y z.
 Definition CR := forall x y, conv x y -> joinable star x y.
 
-Local Hint Resolve starR convR.
+Local Hint Resolve starR convR : core.
 
 Lemma star1 x y : e x y -> star x y.
 Proof. exact: starSE. Qed.
@@ -53,7 +54,7 @@ Lemma starES x y z : e x y -> star y z -> star x z.
 Proof. move/star1. exact: star_trans. Qed.
 
 Lemma star_conv x y : star x y -> conv x y.
-Proof. elim=> //={y} y z _. exact: convSE. Qed.
+Proof. elim=> //={} y z _. exact: convSE. Qed.
 
 Lemma conv1 x y : e x y -> conv x y.
 Proof. exact: convSE. Qed.
@@ -71,7 +72,7 @@ Lemma convESi x y z : e y x -> conv y z -> conv x z.
 Proof. move/conv1i. exact: conv_trans. Qed.
 
 Lemma conv_sym x y : conv x y -> conv y x.
-Proof. elim=> //={y} y z _ ih h; [exact: convESi ih|exact: convES ih]. Qed.
+Proof. elim=> //={} y z _ ih h; [exact: convESi ih|exact: convES ih]. Qed.
 
 Lemma join_conv x y z : star x y -> star z y -> conv x z.
 Proof.
@@ -82,17 +83,17 @@ Lemma confluent_cr :
   confluent <-> CR.
 Proof.
   split=> [h x y|h x y z /star_conv A /star_conv B].
-  - elim=> [|{y} y z _ [u h1 h2] /star1 h3|{y} y z _ [u h1 h2] h3].
+  - elim=> [|{} y z _ [u h1 h2] /star1 h3|{} y z _ [u h1 h2] h3].
     + by exists x.
-    + case: (h y u z h2 h3) => v {h2 h3} h2 h3.
+    + case: (h y u z h2 h3) => v {h3} h2 h3.
       exists v => //. exact: star_trans h2.
     + exists u => //. exact: starES h2.
   - apply: h. apply: conv_trans B. exact: conv_sym.
 Qed.
 
 End Definitions.
 
-Global Hint Resolve starR convR.
+Global Hint Resolve starR convR : core.
 Arguments star_trans {T e} y {x z} A B.
 Arguments conv_trans {T e} y {x z} A B.
 
@@ -193,7 +194,7 @@ Inductive sn x : Prop :=
 Lemma sn_preimage (h : T -> T) x :
   (forall x y, e x y -> e (h x) (h y)) -> sn (h x) -> sn x.
 Proof.
-  move eqn:(h x) => v A B. elim: B h x A eqn => {v} v _ ih h x A eqn.
+  move eqn:(h x) => v A B. elim: B h x A eqn => {} v _ ih h x A eqn.
   apply: SNI => y /A. rewrite eqn => /ih; eauto.
 Qed.
 
@@ -281,7 +282,7 @@ Qed.
 
 Lemma sn_wn x : sn e x -> wn e x.
 Proof.
-  elim=> {x} x _ ih. case (classical x) => [[y exy]|A].
+  elim=> {} x _ ih. case (classical x) => [[y exy]|A].
   - case: (ih _ exy) => z [A B]. exists z. split=> //. exact: starES A.
   - exists x. by split.
 Qed.

examples/ssr/CR.v

@@ -88,7 +88,7 @@ Proof. move<-. exact: pstep_beta. Qed.
 
 Lemma pstep_refl s : pstep s s.
 Proof. elim: s; eauto using pstep. Qed.
-Global Hint Resolve pstep_refl.
+Global Hint Resolve pstep_refl : core.
 
 Lemma step_pstep s t : step s t -> pstep s t.
 Proof. elim; eauto using pstep. Qed.

examples/ssr/POPLmark.v

@@ -66,14 +66,14 @@ where "'SUB' Gamma |- A <: B" := (sub Gamma A B).
 
 Lemma sub_refl Gamma A : SUB Gamma |- A <: A.
 Proof. elim: A Gamma; eauto using sub. Qed.
-Global Hint Resolve sub_refl.
+Global Hint Resolve sub_refl : core.
 
 Lemma sub_ren Gamma Delta xi A B :
   (forall x, x < size Gamma -> xi x < size Delta) ->
   (forall x, x < size Gamma -> Delta`_(xi x) = (Gamma`_x).[ren xi]) ->
   SUB Gamma |- A <: B -> SUB Delta |- A.[ren xi] <: B.[ren xi].
 Proof.
-  move=> sub eqn ty. elim: ty Delta xi sub eqn => {Gamma A B} Gamma //=;
+  move=> sub eqn ty. elim: ty Delta xi sub eqn => {A B} Gamma //=;
     eauto using sub.
   - move=> x A lt _ ih Delta xi sub eqn. apply: sub_var_trans. exact: sub.
     rewrite eqn //. exact: ih.
@@ -94,7 +94,7 @@ Lemma transitivity_proj Gamma A B C :
   transitivity_at B ->
   SUB Gamma |- A <: B -> SUB Gamma |- B <: C -> SUB Gamma |- A <: C.
 Proof. move=> /(_ Gamma A C id). autosubst. Qed.
-Global Hint Resolve transitivity_proj.
+Global Hint Resolve transitivity_proj : core.
 
 Lemma transitivity_ren B xi : transitivity_at B -> transitivity_at B.[ren xi].
 Proof. move=> h Gamma A C zeta. asimpl. exact: h. Qed.
@@ -153,7 +153,7 @@ 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 => {Gamma A B} Gamma...
+  move=> h ty. elim: ty Delta sigma h => {A B} Gamma...
   - 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...
     apply: ih2 => -[_|x /h/sub_weak]. apply: sub_var_trans => //. autosubst.
@@ -247,7 +247,7 @@ Proof with eauto using ty.
     apply. move=> [_|x/h/sub_weak] /=. apply: sub_var_trans => //. autosubst.
     autosubst.
   - move=> Delta1 Gamma A B C s _ ih sub Delta2 sigma h. asimpl.
-    eapply ty_etapp. Focus 2. by eapply ih. autosubst. exact: sub_subst sub.
+    eapply ty_etapp. 2: { by eapply ih. } autosubst. exact: sub_subst sub.
   - move=> Delta1 Gamma A B s _ ih sub Delta2 sigma h.
     eapply ty_sub. by eapply ih. exact: sub_subst sub.
 Qed.
@@ -354,7 +354,7 @@ Definition is_tabs s := if s is TAbs _ _ then true else false.
 Lemma canonical_arr' Delta Gamma s T A B :
   TY Delta;Gamma |- s : T -> SUB Delta |- T <: Arr A B -> value s -> is_abs s.
 Proof.
-  move=> ty. elim: ty A B => //={Delta Gamma s T} Delta Gamma A B s.
+  move=> ty. elim: ty A B => //= {Gamma s T} Delta Gamma A B s.
   - move=> ty _ A' B' sub. by inv sub.
   - move=> _ ih /sub_trans h A' B' /h. exact: ih.
 Qed.
@@ -368,7 +368,7 @@ Qed.
 Lemma canonical_all' Delta Gamma s T A B :
   TY Delta;Gamma |- s : T -> SUB Delta |- T <: All A B -> value s -> is_tabs s.
 Proof.
-  move=> ty. elim: ty A B => //={Delta Gamma s T} Delta Gamma A B s.
+  move=> ty. elim: ty A B => //= {Gamma s T} Delta Gamma A B s.
   - move=> _ _ A' B' sub. by inv sub.
   - move=> _ ih /sub_trans h A' B' /h. exact: ih.
 Qed.

examples/ssr/SystemF_CBV.v

@@ -51,7 +51,7 @@ Inductive eval : term -> term -> Prop :=
     eval (Abs A s) (Abs A s)
 | eval_tabs (A : term) :
     eval (TAbs A) (TAbs A).
-Global Hint Resolve eval_abs eval_tabs.
+Global Hint Resolve eval_abs eval_tabs : core.
 
 (** **** Syntactic typing *)
 
@@ -92,11 +92,11 @@ 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.
-Global Hint Resolve V_value.
+Global Hint Resolve V_value : core.
 
 Lemma V_to_E A rho v : V A rho v -> E A rho v.
 Proof. exists v; eauto. Qed.
-Global Hint Resolve V_to_E.
+Global Hint Resolve V_to_E : core.
 
 Lemma eq_V A rho1 rho2 v :
   (forall X v, eval v v -> (rho1 X v <-> rho2 X v)) -> V A rho1 v -> V A rho2 v.
@@ -119,7 +119,7 @@ Proof.
      (do 2 eexists) => // t /ih1/h[u ev]/ih2 ih; by exists u.
   - move=> A ih rho s xi; asimpl.
     split=> -[s' -> h]; eexists => //; asimpl=> P B; move: {h} (h P B) => [v ev].
-    + move=> /ih {ih} ih. exists v => //. by asimpl in ih.
+    + move=> /ih {} ih. exists v => //. by asimpl in ih.
     + move=> h. exists v => //. apply/ih. autosubst.
 Qed.
 

examples/ssr/SystemF_SN.v

@@ -198,7 +198,7 @@ Definition admissible (rho : nat -> cand) :=
 
 Lemma reducible_sn : reducible sn.
 Proof. constructor; eauto using ARS.sn. by move=> s t [f] /f. Qed.
-Global Hint Resolve reducible_sn.
+Global Hint Resolve reducible_sn : core.
 
 Lemma reducible_var P x : reducible P -> P (TeVar x).
 Proof. move/p_nc. apply=> // t st. inv st. Qed.
@@ -216,7 +216,7 @@ Proof with 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 ns h t la. have snt := p_sn (ih1 _ safe) la.
-      elim: snt la => {t} t _ ih3 la. apply: p_nc... move=> v st. inv st=> //...
+      elim: snt la => {} t _ ih3 la. apply: p_nc... move=> v st. inv st=> //...
       apply: ih3 => //. exact: (p_cl (ih1 _ safe)) la _.
   - constructor.
     + move=> s /(_ sn (TyVar 0) reducible_sn)/p_sn/sn_tclosed; apply.
@@ -251,7 +251,7 @@ Lemma beta_expansion A B rho s t :
   L A rho (App (Abs B s) t).
 Proof with eauto.
   move=> ad snt h. have sns := sn_subst (L_sn ad h).
-  elim: sns t snt h => {s} s sns ih1 t. elim=> {t} t snt ih2 h.
+  elim: sns t snt h => {} s sns ih1 t. elim=> {} t snt ih2 h.
   apply: L_nc => // u st. inv st => //.
   - inv H2. apply: ih1 => //. apply: L_cl ad h _. exact: step_subst.
   - apply: ih2 => //. apply: L_cl_star ad h _. exact: red_beta.
@@ -261,7 +261,7 @@ Lemma inst_expansion A B rho s :
   admissible rho -> L A rho s.|[B/] -> L A rho (TApp (TAbs s) B).
 Proof.
   move=> ad h. have sns := sn_hsubst (L_sn ad h). elim: sns h.
-  move=> {s} s _ ih h. apply: L_nc => // t st. inv st => //.
+  move=> {} s _ ih h. apply: L_nc => // t st. inv st => //.
   inv H2 => //. apply: ih => //. apply: L_cl ad h _. exact: step_hsubst.
 Qed.
 

examples/ssr/pred_CC_omega.v

@@ -152,7 +152,7 @@ Fixpoint rho (s : term) : term :=
 
 Lemma pstep_refl s : pstep s s.
 Proof. elim: s; eauto using pstep. Qed.
-Global Hint Resolve pstep_refl.
+Global Hint Resolve pstep_refl : core.
 
 Lemma step_pstep s t : step s t -> pstep s t.
 Proof. elim; eauto using pstep. Qed.
@@ -206,13 +206,13 @@ Proof.
   apply: (cr_method (e2 := pstep) (rho := rho)).
     exact: step_pstep. exact: pstep_red. exact: rho_triangle.
 Qed.
-Global Hint Resolve church_rosser.
+Global Hint Resolve church_rosser : core.
 
 (** **** Reduction behaviour *)
 
 Lemma normal_step_sort n : normal step (Sort n).
 Proof. move=> [s st]. inv st. Qed.
-Global Hint Resolve normal_step_sort.
+Global Hint Resolve normal_step_sort : core.
 
 CoInductive RedProdSpec A1 B1 : term -> Prop :=
 | RedProdSpecI A2 B2 : red A1 A2 -> red B1 B2 -> RedProdSpec A1 B1 (Prod A2 B2).
@@ -264,7 +264,7 @@ Proof. move/conv_sub1. apply. exact: sub1_refl. Qed.
 
 Lemma sub_refl A : A <: A.
 Proof. apply: sub1_sub. exact: sub1_refl. Qed.
-Global Hint Resolve sub_refl.
+Global Hint Resolve sub_refl : core.
 
 Lemma sub_sort n m : n <= m -> Sort n <: Sort m.
 Proof. move=> leq. exact/sub1_sub/sub1_sort. Qed.
@@ -368,7 +368,7 @@ Notation "[ Gamma |- s ]" := (exists n, [ Gamma |- s :- Sort n ]).
 
 Lemma ty_sort_wf Gamma n : [ Gamma |- Sort n ].
 Proof. exists n.+1. exact: ty_sort. Qed.
-Global Hint Resolve ty_sort_wf ty_sort.
+Global Hint Resolve ty_sort_wf ty_sort : core.
 
 Lemma ty_prod_wf Gamma A B :
   [ Gamma |- A ] -> [ A :: Gamma |- B ] -> [ Gamma |- Prod A B ].
@@ -419,7 +419,7 @@ Proof. move=>->->. exact: weakening. Qed.
 Lemma ty_ok Gamma :
   [ Gamma |- ] -> forall x, x < size Gamma -> [ Gamma |- Gamma`_x ].
 Proof.
-  elim=> // {Gamma} Gamma A n tp _ ih [_|x /ih [{n tp} n tp]];
+  elim=> // {} Gamma A n tp _ ih [_|x /ih [{tp} n tp]];
     exists n; exact: weakening tp.
 Qed.
 

meta.yml

@@ -47,11 +47,15 @@ license:
 
 supported_coq_versions:
   text: 8.14 or later
-  opam: '{(>= "8.14" & < "8.18~") | (= "dev")}'
+  opam: '{(>= "8.14" & < "8.21~") | (= "dev")}'
 
 tested_coq_opam_versions:
 - version: 'coq-dev'
   repo: 'mathcomp/mathcomp-dev'
+- version: '2.2.0-coq-8.19'
+  repo: 'mathcomp/mathcomp'
+- version: '2.1.0-coq-8.18'
+  repo: 'mathcomp/mathcomp'
 - version: '2.0.0-coq-8.17'
   repo: 'mathcomp/mathcomp'
 - version: '1.17.0-coq-8.17'