aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/coqtop.ml
diff options
context:
space:
mode:
authorGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2017-06-15 11:54:45 +0200
committerGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2017-10-06 17:21:46 +0200
commitb0b9ec7c16c38dabc7c4279dbe4d578b74e91c19 (patch)
tree2dbacaa7d6e91c61f29946f38befc05e310d1a59 /toplevel/coqtop.ml
parentf1598b00219a951e94036cb7f48a8fe1309025f1 (diff)
[coqtop] Don't reset coqinit internal variables after initialization.
We remove `init_library_roots` as there is no point in resetting this internal variable. Its only user is `init_load_path` and this function is not meant (and is not) idempotent now.
Diffstat (limited to 'toplevel/coqtop.ml')
-rw-r--r--toplevel/coqtop.ml1
1 files changed, 0 insertions, 1 deletions
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index db7bcb76b..c159a1c6a 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -630,7 +630,6 @@ let init_toplevel arglist =
if (not !Flags.batch_mode || CList.is_empty !compile_list)
&& Global.env_is_initial ()
then Declaremods.start_library !toplevel_name;
- init_library_roots ();
load_vernac_obj ();
require ();
(* XXX: This is incorrect in batch mode, as we will initialize