diff options
Diffstat (limited to 'lib/extract.v')
| -rw-r--r-- | lib/extract.v | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/lib/extract.v b/lib/extract.v index 5c8ff7c..3fee1f7 100644 --- a/lib/extract.v +++ b/lib/extract.v @@ -3,7 +3,8 @@ Pattern.strictly_contains runs. Kept beside the library so the generated module lands where dune collects it. *) -From Stdlib Require Import Extraction ExtrOcamlBasic. +From Stdlib Require Import Extraction ExtrOcamlBasic ExtrOcamlNatInt. Require Import DecreaseChecker. +Require Import Lex. -Extraction "decrease_extracted.ml" contains term_eqb. +Extraction "decrease_extracted.ml" contains term_eqb lex_ltb. |