diff options
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)) |