Merge PR #9013: Do not Export the init modules

3 files changed, 10 insertions, 1 deletions

diff --git a/CHANGES.md b/CHANGES.md
index ca63d60a52..6438cf2571 100644
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -95,6 +95,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.
+
 Universes
 
 - Added `Print Universes Subgraph` variant of `Print Universes`.
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