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 --------------
 1 file changed, 14 deletions(-)

(limited to 'sysinit/coqargs.ml')

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
 
-- 
cgit v1.2.3