blob: 3f8be6f1ee11cd1c06fe954adea86185cf07cb18 (
plain) (
blame)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
|
(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))
|
