Merge pull request #18 from coq-community/mc_1223

Adapt to math-comp/math-comp#1223

.github/workflows/docker-action.yml

@@ -1,3 +1,5 @@
+# This file was generated from `meta.yml`, please do not edit manually.
+# Follow the instructions on https://github.com/coq-community/templates to regenerate.
 name: Docker CI
 
 on:
@@ -16,9 +18,9 @@ jobs:
       matrix:
         image:
           - 'mathcomp/mathcomp-dev:coq-dev'
+          - 'mathcomp/mathcomp-dev:coq-8.19'
           - 'mathcomp/mathcomp-dev:coq-8.18'
-          - 'mathcomp/mathcomp-dev:coq-8.17'
-          - 'mathcomp/mathcomp-dev:coq-8.16'
+          - 'mathcomp/mathcomp:2.2.0-coq-8.19'
           - 'mathcomp/mathcomp:2.1.0-coq-8.18'
           - 'mathcomp/mathcomp:2.1.0-coq-8.17'
           - 'mathcomp/mathcomp:2.1.0-coq-8.16'

README.md

@@ -9,8 +9,8 @@ Follow the instructions on https://github.com/coq-community/templates to regener
 [![Code of Conduct][conduct-shield]][conduct-link]
 [![Zulip][zulip-shield]][zulip-link]
 
-[docker-action-shield]: https://github.com/coq-community/gaia/workflows/Docker%20CI/badge.svg?branch=master
-[docker-action-link]: https://github.com/coq-community/gaia/actions?query=workflow:"Docker%20CI"
+[docker-action-shield]: https://github.com/coq-community/gaia/actions/workflows/docker-action.yml/badge.svg?branch=master
+[docker-action-link]: https://github.com/coq-community/gaia/actions/workflows/docker-action.yml
 
 [contributing-shield]: https://img.shields.io/badge/contributions-welcome-%23f7931e.svg
 [contributing-link]: https://github.com/coq-community/manifesto/blob/master/CONTRIBUTING.md

meta.yml

@@ -78,12 +78,12 @@ dependencies:
 tested_coq_opam_versions:
 - version: 'coq-dev'
   repo: 'mathcomp/mathcomp-dev'
-- version: 'coq-8.18'
-  repo: 'mathcomp/mathcomp-dev'
-- version: 'coq-8.17'
+- version: 'coq-8.19'
   repo: 'mathcomp/mathcomp-dev'
-- version: 'coq-8.16'
+- version: 'coq-8.18'
   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.1.0-coq-8.17'

theories/schutte/ssete9.v

@@ -1918,7 +1918,7 @@ Lemma mul_int n m : \F n * \F m = \F (n *m)%N.
 Proof.
 case: n; first by rewrite T1mul0n.
 move => n;case: m; first by rewrite T1muln0 muln0.
-by move => m /=; rewrite - mulnE mulnSr addnC.
+by move=> m /=; rewrite -?mulnE mulnSr addnC.  (* FIXME: remove -?mulnE when requiring Coq >= 8.21 *)
 Qed.
 
 Lemma mul_phi0 a b: phi0 (a + b) = phi0 a * phi0 b.
@@ -3780,7 +3780,7 @@ Lemma T2addn0: right_id zero T2add.    Proof. by case. Qed.
 
 Lemma add_int n m : \F n + \F m = \F (n +m)%N.
 Proof.
-by case: n m => // n [ | m]; rewrite /= - ? addnS  // - addnE addn0.
+by case: n m => // n [ | m]; rewrite /= - ? addnS  // -?addnE addn0.  (* FIXME: remove -?addnE when requiring Coq >= 8.21 *)
 Qed.
 
 Lemma add_fin_omega n: \F n + omega = omega.

theories/stern/fibm.v

@@ -3965,7 +3965,7 @@ apply:ZeckM_prop3; apply/andP; split.
    by elim:n (0) => // k H n /=; rewrite H eqxx.
 rewrite  /Zeck_val - fib_sum !big_ord_recl /=.
 elim:n => [|n Hr];first by rewrite big_nil big_ord0.
-by rewrite big_ord_recr - (eqP Hr) iota_Sr rev_rcons big_cons addnC.
+by rewrite big_ord_recr 1?addnA -(eqP Hr) iota_Sr rev_rcons big_cons addnC.  (* FIXME: change 1?addnA into addnA when requiring Coq >= 8.21 *)
 Qed.