aboutsummaryrefslogtreecommitdiffhomepage
path: root/META.coq
diff options
context:
space:
mode:
authorGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2017-03-09 01:09:00 +0100
committerGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2017-03-10 16:21:24 +0100
commitccb706774a8f9bf4f58f6899a58e6cc5117901a6 (patch)
tree109928757371fc52805147b2404daf3af859b17e /META.coq
parent7812c5f39dd166559847c1ece573b02653e62100 (diff)
[META] Ltac now a plugin.
Diffstat (limited to 'META.coq')
-rw-r--r--META.coq6
1 files changed, 3 insertions, 3 deletions
diff --git a/META.coq b/META.coq
index dea9fb458..5084237e8 100644
--- a/META.coq
+++ b/META.coq
@@ -263,9 +263,9 @@ package "ltac" (
version = "8.7"
requires = "coq.highparsing"
- directory = "ltac"
+ directory = "plugins/ltac"
- archive(byte) = "ltac.cma"
- archive(native) = "ltac.cmxa"
+ archive(byte) = "ltac_plugin.cmo"
+ archive(native) = "ltac_plugin.cmx"
)