diff options
| author | Gaëtan Gilbert | 2018-11-16 13:32:03 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2018-11-16 13:38:44 +0100 |
| commit | 93ecb0426dafc2654853eba2643ab0c66c3a09f4 (patch) | |
| tree | 203a9b73a4fcd96b7a8264408dea898635615f3a | |
| parent | 778213b89d893b55e572fc1813c7209d647ed6b0 (diff) | |
Do not Export the init modules
It seems we started doing the export silently in
47804492bd09c8b13b5aac45800d067dbdf04d00.
| -rw-r--r-- | CHANGES.md | 4 | ||||
| -rw-r--r-- | test-suite/success/Require.v | 5 | ||||
| -rw-r--r-- | toplevel/coqtop.ml | 2 |
3 files changed, 10 insertions, 1 deletions
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 |