diff options
| author | Pierre-Marie Pédrot | 2018-11-19 13:32:56 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-11-19 13:32:56 +0100 |
| commit | c54edf206c0e3ca58d1d6b1d53ac37267a67415b (patch) | |
| tree | bc9b77e0c5f9188c03369eef3b22ccda615b7c36 /toplevel | |
| parent | ecfbeaa62f9d8bd4dc4600cf39df2262af718313 (diff) | |
| parent | 93ecb0426dafc2654853eba2643ab0c66c3a09f4 (diff) | |
Merge PR #9013: Do not Export the init modules
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/coqtop.ml | 2 |
1 files changed, 1 insertions, 1 deletions
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 |