diff options
| author | Marcos Magueta <maguetamarcos@gmail.com> | 2026-07-11 22:03:21 -0300 |
|---|---|---|
| committer | Marcos Magueta <maguetamarcos@gmail.com> | 2026-07-11 22:03:21 -0300 |
| commit | f22834d3aaed2b2dd2c5d4203e937fc8fb4b5507 (patch) | |
| tree | d1408572183bf8826218b3a067a6c08489f99fe7 /theories/dune | |
| parent | 1832aca3f545f1f6ecadb7e12ed1ce02c2aa78be (diff) | |
| download | SOL-f22834d3aaed2b2dd2c5d4203e937fc8fb4b5507.tar.gz SOL-f22834d3aaed2b2dd2c5d4203e937fc8fb4b5507.zip | |
admission runs the containment checker extracted from rocq
Diffstat (limited to 'theories/dune')
| -rw-r--r-- | theories/dune | 13 |
1 files changed, 10 insertions, 3 deletions
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)) |