aboutsummaryrefslogtreecommitdiff
path: root/plugins/ssr/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/ssr/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/ssr/plugin_base.dune')
-rw-r--r--plugins/ssr/plugin_base.dune1
1 files changed, 1 insertions, 0 deletions
diff --git a/plugins/ssr/plugin_base.dune b/plugins/ssr/plugin_base.dune
index de9053f1a0..a13524bb52 100644
--- a/plugins/ssr/plugin_base.dune
+++ b/plugins/ssr/plugin_base.dune
@@ -3,4 +3,5 @@
(public_name coq.plugins.ssreflect)
(synopsis "Coq's ssreflect plugin")
(modules_without_implementation ssrast)
+ (flags :standard -open Gramlib)
(libraries coq.plugins.ssrmatching))