aboutsummaryrefslogtreecommitdiffstats
path: root/theories/dune
diff options
context:
space:
mode:
Diffstat (limited to 'theories/dune')
-rw-r--r--theories/dune9
1 files changed, 8 insertions, 1 deletions
diff --git a/theories/dune b/theories/dune
index 57cccb6..bde0f7f 100644
--- a/theories/dune
+++ b/theories/dune
@@ -22,6 +22,13 @@
(setenv OCAMLPATH ""
(run coqc -q Lex.v))))
+(rule
+ (targets Interval.vo Interval.glob)
+ (deps Interval.v)
+ (action
+ (setenv OCAMLPATH ""
+ (run coqc -q Interval.v))))
+
(alias
(name default)
- (deps Decrease.vo DecreaseChecker.vo Lex.vo))
+ (deps Decrease.vo DecreaseChecker.vo Lex.vo Interval.vo))