Support Coq 8.19

AU-COBRA · Jun 26, 2024 · 234be25 · 234be25
1 parent 4e5ed5d
commit 234be25
Show file tree

Hide file tree

Showing 3 changed files with 14 additions and 13 deletions.
diff --git a/.github/coq-concert.opam.locked b/.github/coq-concert.opam.locked
@@ -10,15 +10,15 @@ homepage: "https://github.com/AU-COBRA/ConCert"
 doc: "https://au-cobra.github.io/ConCert/toc.html"
 bug-reports: "https://github.com/AU-COBRA/ConCert/issues"
 depends: [
-  "coq" {= "8.18.0"}
-  "coq-bignums" {= "9.0.0+coq8.18"}
-  "coq-metacoq-common" {= "1.3.1+8.18"}
-  "coq-metacoq-erasure" {= "1.3.1+8.18"}
-  "coq-metacoq-pcuic" {= "1.3.1+8.18"}
-  "coq-metacoq-safechecker" {= "1.3.1+8.18"}
-  "coq-metacoq-template" {= "1.3.1+8.18"}
-  "coq-metacoq-template-pcuic" {= "1.3.1+8.18"}
-  "coq-metacoq-utils" {= "1.3.1+8.18"}
+  "coq" {= "8.19.0"}
+  "coq-bignums" {= "9.0.0+coq8.19"}
+  "coq-metacoq-common" {= "1.3.1+8.19"}
+  "coq-metacoq-erasure" {= "1.3.1+8.19"}
+  "coq-metacoq-pcuic" {= "1.3.1+8.19"}
+  "coq-metacoq-safechecker" {= "1.3.1+8.19"}
+  "coq-metacoq-template" {= "1.3.1+8.19"}
+  "coq-metacoq-template-pcuic" {= "1.3.1+8.19"}
+  "coq-metacoq-utils" {= "1.3.1+8.19"}
   "coq-rust-extraction" {= "dev"}
   "coq-elm-extraction" {= "dev"}
   "coq-quickchick" {= "dev"}
@@ -45,6 +45,6 @@ pin-depends: [
   ]
   [
     "coq-quickchick.dev"
-    "git+https://github.com/4ever2/QuickChick.git#bc61d58045feeb754264df9494965c280e266e1c"
+    "git+https://github.com/4ever2/QuickChick.git#d8c1ccf217cc9a56292355474725bc25df40992d"
   ]
 ]
diff --git a/coq-concert.opam b/coq-concert.opam
@@ -14,7 +14,7 @@ bug-reports: "https://github.com/AU-COBRA/ConCert/issues"
 doc: "https://au-cobra.github.io/ConCert/toc.html"
 
 depends: [
-  "coq" {>= "8.17" & < "8.19~"}
+  "coq" {>= "8.17" & < "8.20~"}
   "coq-bignums" {>= "8"}
   "coq-quickchick" {= "dev"}
   "coq-metacoq-utils" {>= "1.3.1" & < "1.4~"}
@@ -32,7 +32,7 @@ depends: [
 pin-depends: [
   ["coq-rust-extraction.dev" "git+https://github.com/AU-COBRA/coq-rust-extraction.git#7a5e27c1242abf36cf265e170562a057ac3415f6"]
   ["coq-elm-extraction.dev" "git+https://github.com/AU-COBRA/coq-elm-extraction.git#32eff8eefebc9b2b7fe81c2653559a819740058b"]
-  ["coq-quickchick.dev" "git+https://github.com/4ever2/QuickChick.git#bc61d58045feeb754264df9494965c280e266e1c"]
+  ["coq-quickchick.dev" "git+https://github.com/4ever2/QuickChick.git#d8c1ccf217cc9a56292355474725bc25df40992d"]
 ]
 
 build: [

diff --git a/examples/boardroomVoting/BoardroomVotingTest.v b/examples/boardroomVoting/BoardroomVotingTest.v
@@ -1,4 +1,5 @@
-From Coq Require Import Cyclic31.
+(* From Coq Require Import Cyclic31. *)
+From Coq.Numbers.Cyclic.Int63 Require Import Cyclic63.
 From Coq Require Import List.
 From Coq Require Import Znumtheory.
 From ConCert.Utils Require Import Extras.