From b0b9ec7c16c38dabc7c4279dbe4d578b74e91c19 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Thu, 15 Jun 2017 11:54:45 +0200 Subject: [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. --- toplevel/coqinit.ml | 3 --- toplevel/coqinit.mli | 1 - toplevel/coqtop.ml | 1 - 3 files changed, 5 deletions(-) (limited to 'toplevel') diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml index 5ca886965..1d5406770 100644 --- a/toplevel/coqinit.ml +++ b/toplevel/coqinit.ml @@ -114,9 +114,6 @@ let init_load_path () = (* additional ml directories, given with option -I *) List.iter Mltop.add_ml_dir (List.rev !ml_includes) -let init_library_roots () = - includes := [] - (* Initialises the Ocaml toplevel before launching it, so that it can find the "include" file in the *source* directory *) let init_ocaml_path () = diff --git a/toplevel/coqinit.mli b/toplevel/coqinit.mli index 3432e79cc..1f7fd6ed9 100644 --- a/toplevel/coqinit.mli +++ b/toplevel/coqinit.mli @@ -21,6 +21,5 @@ val push_include : string -> Names.DirPath.t -> bool -> unit val push_ml_include : string -> unit val init_load_path : unit -> unit -val init_library_roots : unit -> unit val init_ocaml_path : unit -> unit 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 -- cgit v1.2.3