From d85f642ab6fcfe69cf94ab3c2d55cf1e777bdd18 Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@cnrs.fr>
Date: Mon, 15 Jul 2024 15:03:51 +0200
Subject: [PATCH] Add Require Extraction in generated Coq code.
Fixes #75.
---
src/coqBackend.ml | 1 +
1 file changed, 1 insertion(+)
diff --git a/src/coqBackend.ml b/src/coqBackend.ml
index 463838cd0..bd60979ac 100644
--- a/src/coqBackend.ml
+++ b/src/coqBackend.ml
@@ -525,6 +525,7 @@ module Run () = struct
List.iter (fun s -> fprintf f "%s\n\n" s.Stretch.stretch_content)
Front.grammar.BasicSyntax.preludes;
+ fprintf f "From Coq.extraction Require Extraction.\n";
fprintf f "From Coq.Lists Require List.\n";
fprintf f "From Coq.PArith Require Import BinPos.\n";
fprintf f "From Coq.NArith Require Import BinNat.\n";
--
GitLab