From be6c50702a07609768804d11e2dc886b2c85ae60 Mon Sep 17 00:00:00 2001 From: Karl Palmskog Date: Fri, 13 Sep 2024 14:55:57 +0200 Subject: [PATCH] fix coqdep issue in Windows for coq-mtac2.1.4+8.19 --- .../coq-mtac2.1.4+8.19/files/declare-module.patch | 11 +++++++++++ released/packages/coq-mtac2/coq-mtac2.1.4+8.19/opam | 1 + 2 files changed, 12 insertions(+) create mode 100644 released/packages/coq-mtac2/coq-mtac2.1.4+8.19/files/declare-module.patch diff --git a/released/packages/coq-mtac2/coq-mtac2.1.4+8.19/files/declare-module.patch b/released/packages/coq-mtac2/coq-mtac2.1.4+8.19/files/declare-module.patch new file mode 100644 index 000000000..c237ecac9 --- /dev/null +++ b/released/packages/coq-mtac2/coq-mtac2.1.4+8.19/files/declare-module.patch @@ -0,0 +1,11 @@ +diff --git a/theories/Base.v b/theories/Base.v +index ae22566..b89da46 100644 +--- a/theories/Base.v ++++ b/theories/Base.v +@@ -1,5 +1,4 @@ +-Declare ML Module "coq-unicoq.plugin". +-Declare ML Module "MetaCoqPlugin:coq-mtac2.plugin". ++Declare ML Module "coq-mtac2.plugin". + + (* Declare ML Module must work without the Requires to be compatible + with async proofs. Running it before them serves as a test diff --git a/released/packages/coq-mtac2/coq-mtac2.1.4+8.19/opam b/released/packages/coq-mtac2/coq-mtac2.1.4+8.19/opam index 8c74f6db2..3fd472975 100644 --- a/released/packages/coq-mtac2/coq-mtac2.1.4+8.19/opam +++ b/released/packages/coq-mtac2/coq-mtac2.1.4+8.19/opam @@ -11,6 +11,7 @@ authors: [ ] license: "MIT" synopsis: "Typed tactic language for Coq" +patches: ["declare-module.patch"] build: [ ["./configure.sh"] [make "-j%{jobs}%"]