; 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))