From eed37d2f3405f3084c0564d616644ef5e84cc940 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= <frederic.blanqui@inria.fr>
Date: Thu, 28 Nov 2024 13:20:26 +0100
Subject: [PATCH] partially revert previous commit: use Require Import instead
 of Require Export for efficiency reason

---
 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