aboutsummaryrefslogtreecommitdiff
path: root/toplevel
diff options
context:
space:
mode:
authorGaëtan Gilbert2021-02-04 12:25:17 +0100
committerGaëtan Gilbert2021-02-04 15:30:30 +0100
commit2edd93eec8e9bd83da2bbb77a904bb290ee7adf3 (patch)
tree4c2793b3f5d2b79ff4c87ae39f61b5c79d3e2fa4 /toplevel
parentdf7d00971e430468cbf57fa6119b7ed5149a9193 (diff)
Remove deprecated -inputstate command line argument
Deprecated since 6dd9e003c289a79b0656e7c6f2cc59935997370c (2014)
Diffstat (limited to 'toplevel')
-rw-r--r--toplevel/coqtop.ml10
1 files changed, 0 insertions, 10 deletions
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index caf86ef870..16028be910 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -35,14 +35,6 @@ let print_header () =
(******************************************************************************)
-(* Input/Output State *)
-(******************************************************************************)
-let inputstate opts =
- Option.iter (fun istate_file ->
- let fname = Loadpath.locate_file (CUnix.make_suffix istate_file ".coq") in
- Vernacstate.System.load fname) opts.inputstate
-
-(******************************************************************************)
(* Fatal Errors *)
(******************************************************************************)
@@ -70,8 +62,6 @@ let init_toplevel { parse_extra; init_extra; usage; initial_args } =
let opts, customopts = Coqinit.parse_arguments ~parse_extra ~usage ~initial_args () in
Stm.init_process (snd customopts);
let injections = Coqinit.init_runtime opts in
- (* Allow the user to load an arbitrary state here *)
- inputstate opts.pre;
(* This state will be shared by all the documents *)
Stm.init_core ();
let customstate = init_extra ~opts customopts injections in