From f22834d3aaed2b2dd2c5d4203e937fc8fb4b5507 Mon Sep 17 00:00:00 2001 From: Marcos Magueta Date: Sat, 11 Jul 2026 22:03:21 -0300 Subject: admission runs the containment checker extracted from rocq --- theories/dune | 13 ++++++++++--- 1 file changed, 10 insertions(+), 3 deletions(-) (limited to 'theories/dune') diff --git a/theories/dune b/theories/dune index 895fc92..3ef9648 100644 --- a/theories/dune +++ b/theories/dune @@ -1,6 +1,6 @@ ; Checked with rocq's coqc directly: the coq.theory stanza trips on -; the devshell's OCaml findlib path, and a plain rule with a clean -; environment is enough to keep the proofs in the default build. +; the devshell's OCaml findlib path, and plain rules with a clean +; environment are enough to keep the proofs in the default build. (rule (targets Decrease.vo Decrease.glob) (deps Decrease.v) @@ -8,6 +8,13 @@ (setenv OCAMLPATH "" (run coqc -q Decrease.v)))) +(rule + (targets DecreaseChecker.vo DecreaseChecker.glob) + (deps DecreaseChecker.v) + (action + (setenv OCAMLPATH "" + (run coqc -q DecreaseChecker.v)))) + (alias (name default) - (deps Decrease.vo)) + (deps Decrease.vo DecreaseChecker.vo)) -- cgit v1.2.3