From 2edd93eec8e9bd83da2bbb77a904bb290ee7adf3 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Thu, 4 Feb 2021 12:25:17 +0100
Subject: Remove deprecated -inputstate command line argument

Deprecated since 6dd9e003c289a79b0656e7c6f2cc59935997370c (2014)
---
 sysinit/coqargs.ml  | 14 --------------
 sysinit/coqargs.mli |  2 --
 toplevel/coqtop.ml  | 10 ----------
 3 files changed, 26 deletions(-)

diff --git a/sysinit/coqargs.ml b/sysinit/coqargs.ml
index 57658a1eac..4655c1fa5b 100644
--- a/sysinit/coqargs.ml
+++ b/sysinit/coqargs.ml
@@ -75,8 +75,6 @@ type coqargs_pre = {
 
   load_vernacular_list : (string * bool) list;
   injections  : injection_command list;
-
-  inputstate  : string option;
 }
 
 type coqargs_query =
@@ -133,7 +131,6 @@ let default_pre = {
   vo_includes  = [];
   load_vernacular_list = [];
   injections   = [];
-  inputstate   = None;
 }
 
 let default_queries = []
@@ -184,14 +181,6 @@ let set_query opts q =
   | Queries queries -> Queries (queries@[q])
   }
 
-let warn_deprecated_inputstate =
-  CWarnings.create ~name:"deprecated-inputstate" ~category:"deprecated"
-         (fun () -> Pp.strbrk "The inputstate option is deprecated and discouraged.")
-
-let set_inputstate opts s =
-  warn_deprecated_inputstate ();
-  { opts with pre = { opts.pre with inputstate = Some s }}
-
 (******************************************************************************)
 (* Parsing helpers                                                            *)
 (******************************************************************************)
@@ -329,9 +318,6 @@ let parse_args ~usage ~init arglist : t * string list =
     |"-init-file" ->
       { oval with config = { oval.config with rcfile = Some (next ()); }}
 
-    |"-inputstate"|"-is" ->
-      set_inputstate oval (next ())
-
     |"-load-vernac-object" ->
       add_vo_require oval (next ()) None None
 
diff --git a/sysinit/coqargs.mli b/sysinit/coqargs.mli
index aef50193f2..4dd3f32ad0 100644
--- a/sysinit/coqargs.mli
+++ b/sysinit/coqargs.mli
@@ -60,8 +60,6 @@ type coqargs_pre = {
 
   load_vernacular_list : (string * bool) list;
   injections  : injection_command list;
-
-  inputstate  : string option;
 }
 
 type coqargs_query =
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index caf86ef870..16028be910 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -34,14 +34,6 @@ let print_header () =
   flush_all ()
 
 
-(******************************************************************************)
-(* 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
-- 
cgit v1.2.3