From c24b28e2aa2b5fec8d70d744709b6bf599809b70 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?=
 <fblanqui@users.noreply.github.com>
Date: Thu, 28 Nov 2024 18:14:12 +0100
Subject: [PATCH] partially revert #1157: use Require Import instead of Require
 Export for efficiency reason (#1158)

---
 src/export/coq.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/export/coq.ml b/src/export/coq.ml
index 1d6552db0..395b15899 100644
--- a/src/export/coq.ml
+++ b/src/export/coq.ml
@@ -354,7 +354,7 @@ let set_requiring : string -> unit = fun f -> require := Some f
 let print : ast -> unit = fun s ->
   let oc = stdout in
   begin match !require with
-  | Some f -> string oc ("Require Export "^f^".\n")
+  | Some f -> string oc ("Require Import "^f^".\n")
   | None -> ()
   end;
   ast oc s