aboutsummaryrefslogtreecommitdiff
path: root/plugins/ssrmatching/plugin_base.dune
diff options
context:
space:
mode:
authorEmilio Jesus Gallego Arias2018-10-08 16:09:49 +0200
committerEmilio Jesus Gallego Arias2018-10-29 01:25:34 +0100
commitcd8b8974e2d62a3c3c4d7572921b5a83cbb8642c (patch)
treed0be5cca13dc62ac91829531e4906733ac35cbb7 /plugins/ssrmatching/plugin_base.dune
parent46ac5393bf8d3dfef069c4190e3bfe6a3b4dcd90 (diff)
[gramlib] Wrap `Gramlib`.
This introduces a bit of noise in the Dune files but for now I think it is the best way to do it.
Diffstat (limited to 'plugins/ssrmatching/plugin_base.dune')
-rw-r--r--plugins/ssrmatching/plugin_base.dune1
1 files changed, 1 insertions, 0 deletions
diff --git a/plugins/ssrmatching/plugin_base.dune b/plugins/ssrmatching/plugin_base.dune
index 06f67c3774..1450a94de1 100644
--- a/plugins/ssrmatching/plugin_base.dune
+++ b/plugins/ssrmatching/plugin_base.dune
@@ -2,4 +2,5 @@
(name ssrmatching_plugin)
(public_name coq.plugins.ssrmatching)
(synopsis "Coq ssrmatching plugin")
+ (flags :standard -open Gramlib)
(libraries coq.plugins.ltac))