aboutsummaryrefslogtreecommitdiff
path: root/dune
diff options
context:
space:
mode:
authorThéo Zimmermann2018-10-08 17:28:46 +0200
committerThéo Zimmermann2018-10-08 17:28:46 +0200
commit2de0af56b813f2004261eb15fe22586105f3c886 (patch)
treeb0d58e179c8637a2a1a19f60fe4028a8b189d51d /dune
parent22e7ae8f9f5d673fd552c30b7709b948bc8f68a5 (diff)
parentedaf8d0a34993ac5fab373128a27417a620643d4 (diff)
Merge PR #8657: [dune] Refactor files following advice from upstream.
Diffstat (limited to 'dune')
-rw-r--r--dune6
1 files changed, 6 insertions, 0 deletions
diff --git a/dune b/dune
index 27c5e972fe..0a0ff213ed 100644
--- a/dune
+++ b/dune
@@ -1,3 +1,9 @@
+; Default flags for all Coq libraries.
+(env
+ (dev (flags :standard -rectypes -w -9-27-50+60))
+ (release (flags :standard -rectypes)))
+
+; Rules for coq_dune
(rule
(targets .vfiles.d)
(deps