Pin MetaCoq 8.19 branch

4ever2 · Jan 16, 2025 · 36da1bd · 36da1bd
1 parent b9530d2
commit 36da1bd
Show file tree

Hide file tree

Showing 3 changed files with 28 additions and 7 deletions.
diff --git a/.github/coq-concert.opam.locked b/.github/coq-concert.opam.locked
@@ -12,18 +12,27 @@ bug-reports: "https://github.com/AU-COBRA/ConCert/issues"
 depends: [
   "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-metacoq-common" {= "1.3.2+8.19"}
+  "coq-metacoq-erasure" {= "1.3.2+8.19"}
+  "coq-metacoq-pcuic" {= "1.3.2+8.19"}
+  "coq-metacoq-safechecker" {= "1.3.2+8.19"}
+  "coq-metacoq-template" {= "1.3.2+8.19"}
+  "coq-metacoq-template-pcuic" {= "1.3.2+8.19"}
+  "coq-metacoq-utils" {= "1.3.2+8.19"}
   "coq-rust-extraction" {= "0.1.0"}
   "coq-elm-extraction" {= "0.1.0"}
   "coq-quickchick" {= "2.0.4"}
   "coq-stdpp" {= "1.10.0"}
 ]
+pin-depends: [
+  ["coq-metacoq-utils.1.3.2+8.19" "git+https://github.com/MetaCoq/metacoq.git#a9f5da7534b62cda3c870e64f00998e7ee5485f5"]
+  ["coq-metacoq-common.1.3.2+8.19" "git+https://github.com/MetaCoq/metacoq.git#a9f5da7534b62cda3c870e64f00998e7ee5485f5"]
+  ["coq-metacoq-template.1.3.2+8.19" "git+https://github.com/MetaCoq/metacoq.git#a9f5da7534b62cda3c870e64f00998e7ee5485f5"]
+  ["coq-metacoq-template-pcuic.1.3.2+8.19" "git+https://github.com/MetaCoq/metacoq.git#a9f5da7534b62cda3c870e64f00998e7ee5485f5"]
+  ["coq-metacoq-pcuic.1.3.2+8.19" "git+https://github.com/MetaCoq/metacoq.git#a9f5da7534b62cda3c870e64f00998e7ee5485f5"]
+  ["coq-metacoq-safechecker.1.3.2+8.19" "git+https://github.com/MetaCoq/metacoq.git#a9f5da7534b62cda3c870e64f00998e7ee5485f5"]
+  ["coq-metacoq-erasure.1.3.2+8.19" "git+https://github.com/MetaCoq/metacoq.git#a9f5da7534b62cda3c870e64f00998e7ee5485f5"]
+]
 build: [
   [make]
   [make "examples"] {with-test}

diff --git a/coq-concert.opam b/coq-concert.opam
@@ -29,6 +29,16 @@ depends: [
   "coq-stdpp" {>= "1.9.0" & < "1.11~"}
 ]
 
+pin-depends: [
+  ["coq-metacoq-utils.1.3.2+8.19" "git+https://github.com/MetaCoq/metacoq.git#a9f5da7534b62cda3c870e64f00998e7ee5485f5"]
+  ["coq-metacoq-common.1.3.2+8.19" "git+https://github.com/MetaCoq/metacoq.git#a9f5da7534b62cda3c870e64f00998e7ee5485f5"]
+  ["coq-metacoq-template.1.3.2+8.19" "git+https://github.com/MetaCoq/metacoq.git#a9f5da7534b62cda3c870e64f00998e7ee5485f5"]
+  ["coq-metacoq-template-pcuic.1.3.2+8.19" "git+https://github.com/MetaCoq/metacoq.git#a9f5da7534b62cda3c870e64f00998e7ee5485f5"]
+  ["coq-metacoq-pcuic.1.3.2+8.19" "git+https://github.com/MetaCoq/metacoq.git#a9f5da7534b62cda3c870e64f00998e7ee5485f5"]
+  ["coq-metacoq-safechecker.1.3.2+8.19" "git+https://github.com/MetaCoq/metacoq.git#a9f5da7534b62cda3c870e64f00998e7ee5485f5"]
+  ["coq-metacoq-erasure.1.3.2+8.19" "git+https://github.com/MetaCoq/metacoq.git#a9f5da7534b62cda3c870e64f00998e7ee5485f5"]
+]
+
 build: [
   [make]
   [make "examples"] {with-test}

diff --git a/extraction/tests/CameLIGOExtractionTests.v b/extraction/tests/CameLIGOExtractionTests.v
@@ -12,6 +12,8 @@ From Coq Require Import String.
 
 Import MCMonadNotation.
 
+Context `{Blockchain.ChainBase}.
+
 Local Close Scope bs_scope.
 Local Open Scope string_scope.