aboutsummaryrefslogtreecommitdiff
path: root/plugins/funind/plugin_base.dune
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/funind/plugin_base.dune')
-rw-r--r--plugins/funind/plugin_base.dune1
1 files changed, 1 insertions, 0 deletions
diff --git a/plugins/funind/plugin_base.dune b/plugins/funind/plugin_base.dune
index 002eb28eea..9f583234d8 100644
--- a/plugins/funind/plugin_base.dune
+++ b/plugins/funind/plugin_base.dune
@@ -2,4 +2,5 @@
(name recdef_plugin)
(public_name coq.plugins.recdef)
(synopsis "Coq's functional induction plugin")
+ (flags :standard -open Gramlib)
(libraries coq.plugins.extraction))