Merge pull request #60 from andres-erbsen/patch-1

Require Znumtheory before using it

Author: CohenCyril

.github/workflows/docker-action.yml

@@ -28,18 +28,19 @@ jobs:
           - 'mathcomp/mathcomp:2.2.0-coq-8.18'
           - 'mathcomp/mathcomp:2.2.0-coq-8.19'
           - 'mathcomp/mathcomp:2.2.0-coq-8.20'
-          - 'mathcomp/mathcomp:2.2.0-coq-dev'
           - 'mathcomp/mathcomp:2.3.0-coq-8.18'
           - 'mathcomp/mathcomp:2.3.0-coq-8.19'
           - 'mathcomp/mathcomp:2.3.0-coq-8.20'
-          - 'mathcomp/mathcomp:2.3.0-coq-dev'
-          - 'mathcomp/mathcomp-dev:coq-8.18'
-          - 'mathcomp/mathcomp-dev:coq-8.19'
+          - 'mathcomp/mathcomp:2.4.0-coq-8.19'
+          - 'mathcomp/mathcomp:2.4.0-coq-8.20'
+          - 'mathcomp/mathcomp:2.4.0-rocq-prover-9.0'
+          - 'mathcomp/mathcomp:2.4.0-rocq-prover-dev'
           - 'mathcomp/mathcomp-dev:coq-8.20'
-          - 'mathcomp/mathcomp-dev:coq-dev'
+          - 'mathcomp/mathcomp-dev:rocq-prover-9.0'
+          - 'mathcomp/mathcomp-dev:rocq-prover-dev'
       fail-fast: false
     steps:
-      - uses: actions/checkout@v3
+      - uses: actions/checkout@v4
       - uses: coq-community/docker-coq-action@v1
         with:
           opam_file: 'coq-mathcomp-zify.opam'

meta.yml

@@ -53,23 +53,25 @@ tested_coq_opam_versions:
   repo: 'mathcomp/mathcomp'
 - version: '2.2.0-coq-8.20'
   repo: 'mathcomp/mathcomp'
-- version: '2.2.0-coq-dev'
-  repo: 'mathcomp/mathcomp'
 - version: '2.3.0-coq-8.18'
   repo: 'mathcomp/mathcomp'
 - version: '2.3.0-coq-8.19'
   repo: 'mathcomp/mathcomp'
 - version: '2.3.0-coq-8.20'
   repo: 'mathcomp/mathcomp'
-- version: '2.3.0-coq-dev'
+- version: '2.4.0-coq-8.19'
+  repo: 'mathcomp/mathcomp'
+- version: '2.4.0-coq-8.20'
+  repo: 'mathcomp/mathcomp'
+- version: '2.4.0-rocq-prover-9.0'
+  repo: 'mathcomp/mathcomp'
+- version: '2.4.0-rocq-prover-dev'
   repo: 'mathcomp/mathcomp'
-- version: 'coq-8.18'
-  repo: 'mathcomp/mathcomp-dev'
-- version: 'coq-8.19'
-  repo: 'mathcomp/mathcomp-dev'
 - version: 'coq-8.20'
   repo: 'mathcomp/mathcomp-dev'
-- version: 'coq-dev'
+- version: 'rocq-prover-9.0'
+  repo: 'mathcomp/mathcomp-dev'
+- version: 'rocq-prover-dev'
   repo: 'mathcomp/mathcomp-dev'
 
 dependencies:

theories/zify_ssreflect.v

@@ -1,5 +1,6 @@
 From Coq Require Import ZArith ZifyClasses ZifyInst ZifyBool.
 From Coq Require Export Lia.
+From Coq Require Znumtheory.
 
 From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq path.
 From mathcomp Require Import div choice fintype tuple finfun bigop finset prime.