From b7ab0a9d1f0275db32a526faf7cffe9d520b15c8 Mon Sep 17 00:00:00 2001
From: Marcos Magueta <maguetamarcos@gmail.com>
Date: Sun, 12 Jul 2026 10:20:13 -0300
Subject: interval characterization proofs and worked examples

---
 theories/dune | 9 ++++++++-
 1 file changed, 8 insertions(+), 1 deletion(-)

(limited to 'theories/dune')

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))
-- 
cgit v1.2.3