Merge pull request #3155 from palmskog/mtac2-8.19-win-patch

fix coqdep issue in Windows for coq-mtac2.1.4+8.19
coq · Sep 13, 2024 · b26ff98 · b26ff98
2 parents 8858214 + be6c507
commit b26ff98
Show file tree

Hide file tree

Showing 2 changed files with 12 additions and 0 deletions.
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
@@ -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
@@ -11,6 +11,7 @@ authors: [
 ]
 license: "MIT"
 synopsis: "Typed tactic language for Coq"
+patches: ["declare-module.patch"]
 build: [
   ["./configure.sh"]
   [make "-j%{jobs}%"]