Support Coq 8.19

4ever2 · Jan 16, 2025 · b015a0a · b015a0a
1 parent afc60dd
commit b015a0a
Show file tree

Hide file tree

Showing 3 changed files with 12 additions and 11 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" {= "2.0.4"}

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" {>= "2.0.4"}
   "coq-metacoq-utils" {>= "1.3.1" & < "1.4~"}

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.