aboutsummaryrefslogtreecommitdiff
path: root/src/dune
diff options
context:
space:
mode:
authorEmilio Jesus Gallego Arias2018-12-17 19:01:04 +0100
committerEmilio Jesus Gallego Arias2019-02-09 17:46:36 +0100
commit67cff8c545a25e7fa1a29b08d41fc64a7278508b (patch)
tree99f3a46374bdecb25f16bd1109f6d8e690071841 /src/dune
parent2216604fb42a4fe2013e25d95e0c6a5f715db287 (diff)
[coq] Adapt to coq/coq#9137
To be merged when the upstream PR is merged. Not sure this is the right thing to do tho.
Diffstat (limited to 'src/dune')
-rw-r--r--src/dune1
1 files changed, 1 insertions, 0 deletions
diff --git a/src/dune b/src/dune
index 7c911fb041..4a018adb9a 100644
--- a/src/dune
+++ b/src/dune
@@ -2,6 +2,7 @@
(name ltac2)
(public_name coq.plugins.ltac2)
(modules_without_implementation tac2expr tac2qexpr tac2types)
+ (flags :standard -w -50)
(libraries coq.plugins.firstorder))
(rule