admission runs the containment checker extracted from rocq

1 files changed, 9 insertions, 0 deletions

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