blob: 5c8ff7c1f1bf6fe55357386674b6b7d5210acf8d (
plain) (
blame)
1
2
3
4
5
6
7
8
9
|
(* Extraction driver: turns the proven checker of
theories/DecreaseChecker.v into lib/decrease_extracted.ml, which
Pattern.strictly_contains runs. Kept beside the library so the
generated module lands where dune collects it. *)
From Stdlib Require Import Extraction ExtrOcamlBasic.
Require Import DecreaseChecker.
Extraction "decrease_extracted.ml" contains term_eqb.
|
