[CI] adding master

Co-Authored-By: Pierre Roux <[email protected]>

.github/workflows/docker-action.yml

@@ -21,8 +21,11 @@ jobs:
           - 'mathcomp/mathcomp:1.12.0-coq-8.14'
           - 'mathcomp/mathcomp:1.13.0-coq-8.13'
           - 'mathcomp/mathcomp:1.13.0-coq-8.14'
+          - 'mathcomp/mathcomp:1.13.0-coq-8.15'
+          - 'mathcomp/mathcomp:1.13.0-coq-dev'
           - 'mathcomp/mathcomp-dev:coq-8.13'
           - 'mathcomp/mathcomp-dev:coq-8.14'
+          - 'mathcomp/mathcomp-dev:coq-dev'
       fail-fast: false
     steps:
       - uses: actions/checkout@v2

.github/workflows/nix-action-8.13.yml

@@ -16,7 +16,7 @@ jobs:
         fetch-depth: 0
         ref: ${{ env.tested_commit }}
     - name: Cachix install
-      uses: cachix/install-nix-action@v14
+      uses: cachix/install-nix-action@v16
       with:
         nix_path: nixpkgs=channel:nixpkgs-unstable
     - name: Cachix setup math-comp
@@ -53,7 +53,7 @@ jobs:
         fetch-depth: 0
         ref: ${{ env.tested_commit }}
     - name: Cachix install
-      uses: cachix/install-nix-action@v14
+      uses: cachix/install-nix-action@v16
       with:
         nix_path: nixpkgs=channel:nixpkgs-unstable
     - name: Cachix setup math-comp

.github/workflows/nix-action-8.14.yml

@@ -16,7 +16,7 @@ jobs:
         fetch-depth: 0
         ref: ${{ env.tested_commit }}
     - name: Cachix install
-      uses: cachix/install-nix-action@v14
+      uses: cachix/install-nix-action@v16
       with:
         nix_path: nixpkgs=channel:nixpkgs-unstable
     - name: Cachix setup math-comp
@@ -53,7 +53,7 @@ jobs:
         fetch-depth: 0
         ref: ${{ env.tested_commit }}
     - name: Cachix install
-      uses: cachix/install-nix-action@v14
+      uses: cachix/install-nix-action@v16
       with:
         nix_path: nixpkgs=channel:nixpkgs-unstable
     - name: Cachix setup math-comp

.nix/config.nix

@@ -40,6 +40,16 @@
   bundles."8.13".coqPackages.coq.override.version = "8.13";
   bundles."8.14".coqPackages.coq.override.version = "8.14";
 
+  bundles."master".coqPackages = {
+    coq.override.version = "master";
+    coq-elpi.override.version = "coq-master";
+    hierarchy-builder.override.version = "v1.2.1";
+    mathcomp-bigenough.override.version = "1.0.1";
+    mathcomp-finmap.override.version = "1.5.1";
+    mathcomp-real-closed.override.version = "1.1.2";
+    mathcomp.override.version = "1.13.0";
+  };
+
   ## Cachix caches to use in CI
   ## Below we list some standard ones
   cachix.coq = {};

.nix/coq-nix-toolbox.nix

@@ -1 +1 @@
-"f8a44a0138a9f09fe8acc16082196489ab83d39e"
+"ccef60688648484a499d367b1e916e8bd36db789"

README.md

@@ -37,7 +37,7 @@ the Coq proof-assistant and using the Mathematical Components library.
   - Pierre-Yves Strub (initial)
   - Laurent Théry
 - License: [CeCILL-C](LICENSE)
-- Compatible Coq versions: Coq 8.13 to 8.14 (or dev)
+- Compatible Coq versions: Coq 8.13 to 8.15 (or dev)
 - Additional dependencies:
   - [MathComp ssreflect 1.12 or later](https://math-comp.github.io)
   - [MathComp fingroup 1.12 or later](https://math-comp.github.io)

coq-mathcomp-analysis.opam

@@ -18,7 +18,7 @@ the Coq proof-assistant and using the Mathematical Components library."""
 build: [make "-j%{jobs}%"]
 install: [make "install"]
 depends: [
-  "coq" { (>= "8.13" & < "8.15~") | (= "dev") }
+  "coq" { (>= "8.13" & < "8.16~") | (= "dev") }
   "coq-mathcomp-ssreflect" { (>= "1.12.0" & < "1.14~") | (= "dev") }
   "coq-mathcomp-fingroup" { (>= "1.12.0" & < "1.14~") | (= "dev") }
   "coq-mathcomp-algebra" { (>= "1.12.0" & < "1.14~") | (= "dev") }

meta.yml

@@ -49,8 +49,8 @@ license:
   file: LICENSE
 
 supported_coq_versions:
-  text: Coq 8.13 to 8.14 (or dev)
-  opam: '{ (>= "8.13" & < "8.15~") | (= "dev") }'
+  text: Coq 8.13 to 8.15 (or dev)
+  opam: '{ (>= "8.13" & < "8.16~") | (= "dev") }'
 
 tested_coq_opam_versions:
 - version: '1.12.0-coq-8.13'
@@ -61,10 +61,16 @@ tested_coq_opam_versions:
   repo: 'mathcomp/mathcomp'
 - version: '1.13.0-coq-8.14'
   repo: 'mathcomp/mathcomp'
+- version: '1.13.0-coq-8.15'
+  repo: 'mathcomp/mathcomp'
+- version: '1.13.0-coq-dev'
+  repo: 'mathcomp/mathcomp'
 - version: 'coq-8.13'
   repo: 'mathcomp/mathcomp-dev'
 - version: 'coq-8.14'
   repo: 'mathcomp/mathcomp-dev'
+- version: 'coq-dev'
+  repo: 'mathcomp/mathcomp-dev'
 
 dependencies:
 - opam:

theories/normedtype.v

@@ -2893,18 +2893,16 @@ split=> [Ax|[a_ [aTA a_x] ax]]; last first.
   by apply aTA; exists n.
   by apply a_U; near: n; exists m.
 pose U := fun n : nat => [set z : T | `|x - z| < n.+1%:R^-1].
-suff [a_ anx] : exists a_, forall n, a_ n != x /\ (U n `&` A) (a_ n).
+suff /(_ _)/cid-/all_sig[a_ anx] : forall n, exists a, a != x /\ (U n `&` A) a.
   exists a_; split.
   - by move=> a [n _ <-]; have [? []] := anx n.
   - by move=> n; have [] := anx n.
   - apply/cvg_distP => _/posnumP[e]; rewrite near_map; near=> n.
     have [? [] Uan Aan] := anx n.
     by rewrite (lt_le_trans Uan)// ltW//; near: n; exact: near_infty_natSinv_lt.
-have @a_ : nat -> T.
-  move=> n; have : nbhs (x : T) (U n).
-    by apply/(nbhs_ballP (x:T) (U n)); rewrite nbhs_ballE; exists n.+1%:R^-1.
-  by move/Ax/cid => [/= an [anx Aan Uan]]; exact: an.
-by exists a_ => n; rewrite /a_ /= /ssr_have; case: cid => ? [].
+move=> n; have : nbhs (x : T) (U n).
+  by apply/(nbhs_ballP (x:T) (U n)); rewrite nbhs_ballE; exists n.+1%:R^-1.
+by move/Ax/cid => [/= an [anx Aan Uan]]; exists an.
 Unshelve. all: by end_near. Qed.
 
 Section open_closed_sets.

theories/sequences.v

@@ -1564,7 +1564,7 @@ rewrite lee_pmul//.
 - rewrite -(@fineK _ (g n)) ?lee_fin; last by near: n; exact: gfin.
   near: n; apply: (cvg_gt_ge gb) => //.
   by rewrite ltr_pdivr_mulr// ltr_pmulr// ltr1n.
-Grab Existential Variables. all: end_near. Qed.
+Unshelve. all: end_near. Qed.
 
 Lemma ereal_cvgM_lt0_pinfty (R : realFieldType) (f g : (\bar R)^nat) b :
   (b < 0)%R -> f --> +oo -> g --> b%:E -> f \* g --> -oo.
@@ -1580,7 +1580,7 @@ rewrite lee_pmul//.
 - rewrite EFinM EFinN mulNe lee_opp.
   rewrite -(@fineK _ (g n)) ?lee_fin; last by near: n; exact: gfin.
   by near: n; apply: (cvg_lt_le gb) => //; rewrite ltr_nmulr// invf_lt1// ltr1n.
-Grab Existential Variables. all: end_near. Qed.
+Unshelve. all: end_near. Qed.
 
 Lemma ereal_cvgM_gt0_ninfty (R : realFieldType) (f g : (\bar R)^nat) b :
   (0 < b)%R -> f --> -oo -> g --> b%:E -> f \* g --> -oo.
@@ -1648,7 +1648,7 @@ move=> [:apoo] [:bnoo] [:poopoo] [:poonoo]; move: a b => [a| |] [b| |] //.
 - move=> _ foo goo; rewrite mule_ninfty_ninfty -mule_pinfty_pinfty.
   by under eq_fun do rewrite -muleNN; apply: poopoo;
     rewrite -/(- -oo); apply: ereal_cvgN.
-Grab Existential Variables. all: end_near. Qed.
+Unshelve. all: end_near. Qed.
 
 Lemma ereal_lim_sum (R : realFieldType) (I : Type) (r : seq I)
     (f : I -> (\bar R)^nat) (l : I -> \bar R) (P : pred I) :