blob: 895fc92cde4277faf837031df3c67f3aec7beb68 (
plain) (
blame)
1
2
3
4
5
6
7
8
9
10
11
12
13
|
; 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.
(rule
(targets Decrease.vo Decrease.glob)
(deps Decrease.v)
(action
(setenv OCAMLPATH ""
(run coqc -q Decrease.v))))
(alias
(name default)
(deps Decrease.vo))
|
