aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2017-06-13 14:19:37 +0200
committerGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2017-07-17 11:50:41 +0200
commit99e84da08f7a38ac70d90d21d644b4a9a4a80c91 (patch)
treea35446caadf0ad26f4a9e203d5d038e0915d5ac3
parent3a5dd0df47b83a1a46061f2a14761d3d9ad79fcb (diff)
[meta] [api] Fix META file for API introduction.
-rw-r--r--META.coq44
1 files changed, 24 insertions, 20 deletions
diff --git a/META.coq b/META.coq
index 5bf7a000c..e70b8e28d 100644
--- a/META.coq
+++ b/META.coq
@@ -95,6 +95,8 @@ package "intf" (
directory = "intf"
+ archive(byte) = "intf.cma"
+ archive(native) = "intf.cmxa"
)
package "engine" (
@@ -239,19 +241,6 @@ package "toplevel" (
)
-package "highparsing" (
-
- description = "Coq Extra Parsing"
- version = "8.7"
-
- requires = "coq.toplevel"
- directory = "parsing"
-
- archive(byte) = "highparsing.cma"
- archive(native) = "highparsing.cmxa"
-
-)
-
package "idetop" (
description = "Coq IDE Libraries"
@@ -279,28 +268,43 @@ package "ide" (
)
-package "ltac" (
+# XXX: Remove the dependency on toplevel (due to Coqinit use for compat flags)
+package "highparsing" (
- description = "Coq LTAC Plugin"
+ description = "Coq Extra Parsing"
version = "8.7"
- requires = "coq.highparsing"
- directory = "plugins/ltac"
+ requires = "coq.toplevel"
+ directory = "parsing"
- archive(byte) = "ltac_plugin.cmo"
- archive(native) = "ltac_plugin.cmx"
+ archive(byte) = "highparsing.cma"
+ archive(native) = "highparsing.cmxa"
)
+# XXX: API should depend only on stm.
package "API" (
description = "Coq API"
version = "8.7"
- requires = "coq.toplevel"
+ requires = "coq.highparsing"
directory = "API"
archive(byte) = "API.cma"
archive(native) = "API.cmxa"
)
+
+package "ltac" (
+
+ description = "Coq LTAC Plugin"
+ version = "8.7"
+
+ requires = "coq.API"
+ directory = "plugins/ltac"
+
+ archive(byte) = "ltac_plugin.cmo"
+ archive(native) = "ltac_plugin.cmx"
+
+)