From e56efc19f71898d798c44b5955fe74451ee0fc6f Mon Sep 17 00:00:00 2001
From: Marcos Magueta <maguetamarcos@gmail.com>
Date: Sun, 12 Jul 2026 10:07:23 -0300
Subject: lexicographic order proven well founded, checker extracted and
 verifying admission

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

(limited to 'theories/dune')

diff --git a/theories/dune b/theories/dune
index 3ef9648..57cccb6 100644
--- a/theories/dune
+++ b/theories/dune
@@ -15,6 +15,13 @@
   (setenv OCAMLPATH ""
    (run coqc -q DecreaseChecker.v))))
 
+(rule
+ (targets Lex.vo Lex.glob)
+ (deps Lex.v DecreaseChecker.vo)
+ (action
+  (setenv OCAMLPATH ""
+   (run coqc -q Lex.v))))
+
 (alias
  (name default)
- (deps Decrease.vo DecreaseChecker.vo))
+ (deps Decrease.vo DecreaseChecker.vo Lex.vo))
-- 
cgit v1.2.3