aboutsummaryrefslogtreecommitdiff
path: root/plugins/ltac/plugin_base.dune
diff options
context:
space:
mode:
authorEnrico Tassi2018-11-21 17:13:12 +0100
committerEnrico Tassi2018-11-21 17:13:12 +0100
commitabcc20d6a3aebee36160cd17b1f80c56f39876f3 (patch)
tree8c4da66c6a8e3ce515344db3752527cdff6ab2e0 /plugins/ltac/plugin_base.dune
parentd6a53754602dd606644f90b3b6fb8fc82db6d373 (diff)
parent002a974b66bc5b8524c8c045d6b9ec4f57aa7734 (diff)
Merge PR #8985: [gramlib] [build] Switch make-based system to packed gramlib
Diffstat (limited to 'plugins/ltac/plugin_base.dune')
-rw-r--r--plugins/ltac/plugin_base.dune1
1 files changed, 0 insertions, 1 deletions
diff --git a/plugins/ltac/plugin_base.dune b/plugins/ltac/plugin_base.dune
index 1b31655310..5611f5ba16 100644
--- a/plugins/ltac/plugin_base.dune
+++ b/plugins/ltac/plugin_base.dune
@@ -3,7 +3,6 @@
(public_name coq.plugins.ltac)
(synopsis "Coq's LTAC tactic language")
(modules :standard \ tauto)
- (flags :standard -open Gramlib)
(libraries coq.stm))
(library