Merge PR #9887: [api] Remove 8.10 deprecations.

Reviewed-by: SkySkimmer

3 files changed, 0 insertions, 47 deletions

diff --git a/toplevel/coqargs.ml b/toplevel/coqargs.ml
index 9a18baa0bc..ec43dbb1d7 100644
--- a/toplevel/coqargs.ml
+++ b/toplevel/coqargs.ml
@@ -184,10 +184,6 @@ let warn_deprecated_inputstate =
   CWarnings.create ~name:"deprecated-inputstate" ~category:"deprecated"
          (fun () -> Pp.strbrk "The inputstate option is deprecated and discouraged.")
 
-let warn_deprecated_boot =
-  CWarnings.create ~name:"deprecated-boot" ~category:"noop"
-         (fun () -> Pp.strbrk "The -boot option is deprecated, please use -q and/or -coqlib options instead.")
-
 let set_inputstate opts s =
   warn_deprecated_inputstate ();
   { opts with inputstate = Some s }
@@ -488,9 +484,6 @@ let parse_args ~help ~init arglist : t * string list =
       { oval with batch = true }
     |"-test-mode" -> Vernacentries.test_mode := true; oval
     |"-beautify" -> Flags.beautify := true; oval
-    |"-boot" ->
-      warn_deprecated_boot ();
-      { oval with load_rcfile = false; }
     |"-bt" -> Backtrace.record_backtrace true; oval
     |"-color" -> set_color oval (next ())
     |"-config"|"--config" -> { oval with print_config = true }
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 9323a57417..b769405cf6 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -271,31 +271,6 @@ let init_toploop opts =
   let state = { doc; sid; proof = None; time = opts.time } in
   Ccompile.load_init_vernaculars opts ~state, opts
 
-(* To remove in 8.11 *)
-let call_coqc args =
-  let remove str arr = Array.(of_list List.(filter (fun l -> not String.(equal l str)) (to_list arr))) in
-  let coqc_name = Filename.remove_extension (System.get_toplevel_path "coqc") in
-  let args = remove "-compile" args in
-  Unix.execv coqc_name args
-
-let deprecated_coqc_warning = CWarnings.(create
-    ~name:"deprecate-compile-arg"
-    ~category:"toplevel"
-    ~default:Enabled
-    (fun opt_name -> Pp.(seq [str "The option "; str opt_name; str" is deprecated, please use coqc."])))
-
-let rec coqc_deprecated_check args acc extras =
-  match extras with
-  | [] -> acc
-  | "-o" :: _ :: rem ->
-    deprecated_coqc_warning "-o";
-    coqc_deprecated_check args acc rem
-  | ("-compile"|"-compile-verbose") :: file :: rem ->
-    deprecated_coqc_warning "-compile";
-    call_coqc args
-  | x :: rem ->
-    coqc_deprecated_check args (x::acc) rem
-
 let coqtop_init ~opts extra =
   init_color opts;
   CoqworkmgrApi.(init !async_proofs_worker_priority);
@@ -317,7 +292,6 @@ let start_coq custom =
         init_toplevel
           ~help:Usage.print_usage_coqtop ~init:default custom.init
           (List.tl (Array.to_list Sys.argv)) in
-      let extras = coqc_deprecated_check Sys.argv [] extras in
       if not (CList.is_empty extras) then begin
         prerr_endline ("Don't know what to do with "^String.concat " " extras);
         prerr_endline "See -help for the list of supported options";
diff --git a/toplevel/usage.ml b/toplevel/usage.ml
index 7074215afe..da2094653b 100644
--- a/toplevel/usage.ml
+++ b/toplevel/usage.ml
@@ -102,12 +102,6 @@ let print_usage_coqtop () =
 coqtop specific options:\
 \n\
 \n  -batch                 batch mode (exits just after argument parsing)\
-\n\
-\nDeprecated options [use coqc instead]:\
-\n\
-\n  -compile f.v           compile Coq file f.v (implies -batch)\
-\n  -compile-verbose f.v   verbosely compile Coq file f.v (implies -batch)\
-\n  -o f.vo                use f.vo as the output file name\
 \n";
   flush stderr ;
   exit 1
@@ -128,14 +122,6 @@ coqc specific options:\
 \nUndocumented:\
 \n  -vio2vo                [see manual]\
 \n  -check-vio-tasks       [see manual]\
-\n\
-\nDeprecated options:\
-\n\
-\n  -image f               specify an alternative executable for Coq\
-\n  -opt                   run the native-code version of Coq\
-\n  -byte                  run the bytecode version of Coq\
-\n  -t                     keep temporary files\
-\n  -outputstate file      save summary state in file \
 \n";
   flush stderr ;
   exit 1