From f22834d3aaed2b2dd2c5d4203e937fc8fb4b5507 Mon Sep 17 00:00:00 2001
From: Marcos Magueta <maguetamarcos@gmail.com>
Date: Sat, 11 Jul 2026 22:03:21 -0300
Subject: admission runs the containment checker extracted from rocq

---
 lib/dune | 9 +++++++++
 1 file changed, 9 insertions(+)

(limited to 'lib/dune')

diff --git a/lib/dune b/lib/dune
index 2d9154e..3f8be6f 100644
--- a/lib/dune
+++ b/lib/dune
@@ -3,6 +3,15 @@
  (public_name sol)
  (libraries zarith))
 
+; The proven containment checker, extracted from Rocq. The .v files
+; are the source of truth; the generated module is a build artifact.
+(rule
+ (targets decrease_extracted.ml decrease_extracted.mli)
+ (deps extract.v ../theories/DecreaseChecker.vo)
+ (action
+  (setenv OCAMLPATH ""
+   (run coqc -q -Q ../theories "" extract.v))))
+
 (ocamllex lexer)
 
 (menhir
-- 
cgit v1.2.3