From 93ecb0426dafc2654853eba2643ab0c66c3a09f4 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Fri, 16 Nov 2018 13:32:03 +0100
Subject: Do not Export the init modules

It seems we started doing the export silently in
47804492bd09c8b13b5aac45800d067dbdf04d00.
---
 CHANGES.md                   | 4 ++++
 test-suite/success/Require.v | 5 +++++
 toplevel/coqtop.ml           | 2 +-
 3 files changed, 10 insertions(+), 1 deletion(-)

diff --git a/CHANGES.md b/CHANGES.md
index e280cc2fb5..d7f2107d1f 100644
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -93,6 +93,10 @@ Standard Library
 
 - Added `ByteVector` type that can convert to and from [string].
 
+- The prelude used to be automatically Exported and is now only
+  Imported. This should be relevant only when importing files which
+  don't use -noinit into files which do.
+
 Changes from 8.8.2 to 8.9+beta1
 ===============================
 
diff --git a/test-suite/success/Require.v b/test-suite/success/Require.v
index f851d8c7d9..de5987c4f7 100644
--- a/test-suite/success/Require.v
+++ b/test-suite/success/Require.v
@@ -1,3 +1,8 @@
+(* -*- coq-prog-args: ("-noinit"); -*- *)
+
 Require Import Coq.Arith.Plus.
 Require Coq.Arith.Minus.
 Locate Library Coq.Arith.Minus.
+
+(* Check that Init didn't get exported by the import above *)
+Fail Check nat.
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index e4d9e9ac25..66469ff0b9 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -107,7 +107,7 @@ let load_init_vernaculars cur_feeder opts ~state =
 (* Startup LoadPath and Modules                                               *)
 (******************************************************************************)
 (* prelude_data == From Coq Require Export Prelude. *)
-let prelude_data = "Prelude", Some "Coq", Some true
+let prelude_data = "Prelude", Some "Coq", Some false
 
 let require_libs opts =
   if opts.load_init then prelude_data :: opts.vo_requires else opts.vo_requires
-- 
cgit v1.2.3