(library
 (name sol)
 (public_name sol)
 (libraries zarith))

; The proven containment checker, extracted from Rocq. The .v files
; are the source of truth; the generated module is a build artifact.
(rule
 (targets decrease_extracted.ml decrease_extracted.mli)
 (deps extract.v ../theories/DecreaseChecker.vo)
 (action
  (setenv OCAMLPATH ""
   (run coqc -q -Q ../theories "" extract.v))))

(ocamllex lexer)

(menhir
 (modules parser))