Merge pull request #19 from coq-community/dune-0.6

bump to Dune 3.5 or later and Dune-Coq 0.6
coq-community · Jul 24, 2024 · c9a7657 · c9a7657
2 parents 05942fe + d9421f7
commit c9a7657
Show file tree

Hide file tree

Showing 8 changed files with 9 additions and 9 deletions.
diff --git a/.github/workflows/docker-action.yml b/.github/workflows/docker-action.yml
@@ -29,7 +29,7 @@ jobs:
           - 'mathcomp/mathcomp:2.0.0-coq-8.16'
       fail-fast: false
     steps:
-      - uses: actions/checkout@v3
+      - uses: actions/checkout@v4
       - uses: coq-community/docker-coq-action@v1
         with:
           custom_image: ${{ matrix.image }}

diff --git a/coq-gaia-numbers.opam b/coq-gaia-numbers.opam
@@ -14,7 +14,7 @@ Elements of Mathematics in Coq using the Mathematical Components library."""
 
 build: ["dune" "build" "-p" name "-j" jobs]
 depends: [
-  "dune" {>= "2.8"}
+  "dune" {>= "3.5"}
   "coq" {>= "8.16"}
   "coq-mathcomp-ssreflect" {>= "2.0"}
   "coq-mathcomp-algebra"

diff --git a/coq-gaia-ordinals.opam b/coq-gaia-ordinals.opam
@@ -14,7 +14,7 @@ the Mathematical Components library."""
 
 build: ["dune" "build" "-p" name "-j" jobs]
 depends: [
-  "dune" {>= "2.8"}
+  "dune" {>= "3.5"}
   "coq" {>= "8.16"}
   "coq-mathcomp-ssreflect" {>= "2.0"}
   "coq-gaia-theory-of-sets" {= version}

diff --git a/coq-gaia-schutte.opam b/coq-gaia-schutte.opam
@@ -14,7 +14,7 @@ following the approaches of Schütte and Ackermann."""
 
 build: ["dune" "build" "-p" name "-j" jobs]
 depends: [
-  "dune" {>= "2.8"}
+  "dune" {>= "3.5"}
   "coq" {>= "8.16"}
   "coq-mathcomp-ssreflect" {>= "2.0"}
 ]

diff --git a/coq-gaia-stern.opam b/coq-gaia-stern.opam
@@ -14,7 +14,7 @@ Mathematical Components library."""
 
 build: ["dune" "build" "-p" name "-j" jobs]
 depends: [
-  "dune" {>= "2.8"}
+  "dune" {>= "3.5"}
   "coq" {>= "8.16"}
   "coq-mathcomp-ssreflect" {>= "2.0"}
   "coq-mathcomp-algebra"

diff --git a/coq-gaia-theory-of-sets.opam b/coq-gaia-theory-of-sets.opam
@@ -14,7 +14,7 @@ Elements of Mathematics in Coq using the Mathematical Components library."""
 
 build: ["dune" "build" "-p" name "-j" jobs]
 depends: [
-  "dune" {>= "2.8"}
+  "dune" {>= "3.5"}
   "coq" {>= "8.16"}
   "coq-mathcomp-ssreflect" {>= "2.0"}
 ]

diff --git a/dune-project b/dune-project
@@ -1,3 +1,3 @@
-(lang dune 2.8)
-(using coq 0.3)
+(lang dune 3.5)
+(using coq 0.6)
 (name gaia)
diff --git a/theories/numbers/ssetz.v b/theories/numbers/ssetz.v
@@ -386,7 +386,7 @@ Lemma BZopp_sg x: intp x -> x <> \0z ->
 Proof.
 move => pa pb; rewrite /int_np /int_pp.
 have pnz: (P x <> \0c) by move => h; case: pb; apply: BZ_0_if_val0.
-by rewrite /BZopp /BZ_of_nat /BZm_of_nat; Ytac0;Ytac sx; aw; rewrite ? sx. 
+by rewrite /BZopp /BZ_of_nat /BZm_of_nat; Ytac0;Ytac sx; aw; rewrite ? sx; split.
 Qed.
 
 Lemma BZopp_positive1 x: inc x BZps -> inc (BZopp x) BZms.