diff --git a/.github/coq-concert.opam.locked b/.github/coq-concert.opam.locked index 3a56cfdf..543d27ae 100644 --- 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 index 3bb7f005..27bcda1f 100644 --- 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 index ec16eeac..f30b710e 100644 --- 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.