aboutsummaryrefslogtreecommitdiff
path: root/plugins/ltac/plugin_base.dune
diff options
context:
space:
mode:
authorPierre-Marie Pédrot2018-10-29 13:38:29 +0100
committerPierre-Marie Pédrot2018-10-29 13:38:29 +0100
commit35f715a005063a2c6195c574d019ba202bcdc27b (patch)
tree5dc3edf54bc0d3db9a6cbd95f6225b16f36ef3ae /plugins/ltac/plugin_base.dune
parentd838a67707812cb496f0f0f83f1ebe5a65280c86 (diff)
parentcd8b8974e2d62a3c3c4d7572921b5a83cbb8642c (diff)
Merge PR #8667: [RFC] Vendoring of Camlp5
Diffstat (limited to 'plugins/ltac/plugin_base.dune')
-rw-r--r--plugins/ltac/plugin_base.dune1
1 files changed, 1 insertions, 0 deletions
diff --git a/plugins/ltac/plugin_base.dune b/plugins/ltac/plugin_base.dune
index 5611f5ba16..1b31655310 100644
--- a/plugins/ltac/plugin_base.dune
+++ b/plugins/ltac/plugin_base.dune
@@ -3,6 +3,7 @@
(public_name coq.plugins.ltac)
(synopsis "Coq's LTAC tactic language")
(modules :standard \ tauto)
+ (flags :standard -open Gramlib)
(libraries coq.stm))
(library