aboutsummaryrefslogtreecommitdiff
path: root/META.coq
diff options
context:
space:
mode:
Diffstat (limited to 'META.coq')
-rw-r--r--META.coq68
1 files changed, 27 insertions, 41 deletions
diff --git a/META.coq b/META.coq
index e70b8e28df..27aeac61b7 100644
--- a/META.coq
+++ b/META.coq
@@ -228,6 +228,32 @@ package "stm" (
)
+package "API" (
+
+ description = "Coq API"
+ version = "8.7"
+
+ requires = "coq.stm"
+ 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"
+
+)
+
package "toplevel" (
description = "Coq Toplevel"
@@ -254,6 +280,7 @@ package "idetop" (
)
+# XXX Depends on way less than toplevel
package "ide" (
description = "Coq IDE Libraries"
@@ -267,44 +294,3 @@ package "ide" (
archive(native) = "ide.cmxa"
)
-
-# XXX: Remove the dependency on toplevel (due to Coqinit use for compat flags)
-package "highparsing" (
-
- description = "Coq Extra Parsing"
- version = "8.7"
-
- requires = "coq.toplevel"
- directory = "parsing"
-
- 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.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"
-
-)