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