Merge PR #13822: Remove deprecated command line arguments

Reviewed-by: gares

6 files changed, 4 insertions, 35 deletions

diff --git a/doc/changelog/08-cli-tools/13822-rm-depr-cmdline.rst b/doc/changelog/08-cli-tools/13822-rm-depr-cmdline.rst
new file mode 100644
index 0000000000..e3333f8a9a
--- /dev/null
+++ b/doc/changelog/08-cli-tools/13822-rm-depr-cmdline.rst
@@ -0,0 +1,4 @@
+- **Removed:** previously deprecated command line options
+  ``-sprop-cumulative`` and ``-input-state`` and its alias ``-is``
+  (`#13822 <https://github.com/coq/coq/pull/13822>`_,
+  by Gaëtan Gilbert).
diff --git a/sysinit/coqargs.ml b/sysinit/coqargs.ml
index c4f12f6bb7..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,18 +181,6 @@ let set_query opts q =
   | Queries queries -> Queries (queries@[q])
   }
 
-let warn_deprecated_sprop_cumul =
-  CWarnings.create ~name:"deprecated-spropcumul" ~category:"deprecated"
-         (fun () -> Pp.strbrk "Use the \"Cumulative StrictProp\" flag instead.")
-
-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                                                            *)
 (******************************************************************************)
@@ -333,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
 
@@ -419,9 +401,6 @@ let parse_args ~usage ~init arglist : t * string list =
       add_set_option oval Vernacentries.allow_sprop_opt_name (OptionSet None)
     |"-disallow-sprop" ->
       add_set_option oval Vernacentries.allow_sprop_opt_name OptionUnset
-    |"-sprop-cumulative" ->
-      warn_deprecated_sprop_cumul();
-      add_set_option oval Vernacentries.cumul_sprop_opt_name (OptionSet None)
     |"-indices-matter" -> set_logic (fun o -> { o with indices_matter = true }) oval
     |"-m"|"--memory" -> { oval with post = { memory_stat = true }}
     |"-noinit"|"-nois" -> { oval with pre = { oval.pre with load_init = false }}
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/sysinit/usage.ml b/sysinit/usage.ml
index 1831a3f9b2..763cd54137 100644
--- a/sysinit/usage.ml
+++ b/sysinit/usage.ml
@@ -79,7 +79,6 @@ let print_usage_common co command =
 \n  -impredicative-set     set sort Set impredicative\
 \n  -allow-sprop           allow using the proof irrelevant SProp sort\
 \n  -disallow-sprop        forbid using the proof irrelevant SProp sort\
-\n  -sprop-cumulative      make sort SProp cumulative with the rest of the hierarchy\
 \n  -indices-matter        levels of indices (and nonuniform parameters) contribute to the level of inductives\
 \n  -type-in-type          disable universe consistency checking\
 \n  -mangle-names x        mangle auto-generated names using prefix x\
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
diff --git a/vernac/vernacentries.mli b/vernac/vernacentries.mli
index cf233248d7..2ac8458ad5 100644
--- a/vernac/vernacentries.mli
+++ b/vernac/vernacentries.mli
@@ -26,4 +26,3 @@ val interp_redexp_hook : (Environ.env -> Evd.evar_map -> Genredexpr.raw_red_expr
 val command_focus : unit Proof.focus_kind
 
 val allow_sprop_opt_name : string list
-val cumul_sprop_opt_name : string list