admission runs the containment checker extracted from rocq

1 files changed, 9 insertions, 0 deletions

diff --git a/lib/extract.v b/lib/extract.v
new file mode 100644
index 0000000..5c8ff7c
--- /dev/null
+++ b/lib/extract.v
@@ -0,0 +1,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.