From e56efc19f71898d798c44b5955fe74451ee0fc6f Mon Sep 17 00:00:00 2001
From: Marcos Magueta <maguetamarcos@gmail.com>
Date: Sun, 12 Jul 2026 10:07:23 -0300
Subject: lexicographic order proven well founded, checker extracted and
 verifying admission

---
 lib/extract.v | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

(limited to 'lib/extract.v')

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.
-- 
cgit v1.2.3