blob: bde0f7fd2339509b72a1434c18ef00733b9ea509 (
plain) (
blame)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
|
; Checked with rocq's coqc directly: the coq.theory stanza trips on
; 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)
(action
(setenv OCAMLPATH ""
(run coqc -q Decrease.v))))
(rule
(targets DecreaseChecker.vo DecreaseChecker.glob)
(deps DecreaseChecker.v)
(action
(setenv OCAMLPATH ""
(run coqc -q DecreaseChecker.v))))
(rule
(targets Lex.vo Lex.glob)
(deps Lex.v DecreaseChecker.vo)
(action
(setenv OCAMLPATH ""
(run coqc -q Lex.v))))
(rule
(targets Interval.vo Interval.glob)
(deps Interval.v)
(action
(setenv OCAMLPATH ""
(run coqc -q Interval.v))))
(alias
(name default)
(deps Decrease.vo DecreaseChecker.vo Lex.vo Interval.vo))
|
