From e8419bac30ab98527ec6b15d5a0f5c1035539ca5 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Tue, 12 Feb 2019 02:41:00 +0100
Subject: [library] Remove `-boot` option.

The `-boot` option was used to:

- suppress loading of the rc_file
- allow to save modules with prefix `Coq`

There is no good reason disable saving of modules with `Coq` prefix by
default, thus we remove this option.

Fixes: #9575
---
 toplevel/ccompile.ml |  2 --
 toplevel/coqargs.ml  | 12 +++++++-----
 toplevel/coqargs.mli |  2 --
 toplevel/coqtop.ml   |  1 -
 toplevel/usage.ml    |  1 -
 5 files changed, 7 insertions(+), 11 deletions(-)

(limited to 'toplevel')

diff --git a/toplevel/ccompile.ml b/toplevel/ccompile.ml
index 8064ee8880..3fe6ad0718 100644
--- a/toplevel/ccompile.ml
+++ b/toplevel/ccompile.ml
@@ -112,7 +112,6 @@ let compile opts copts ~echo ~f_in ~f_out =
       let doc, sid = Topfmt.(in_phase ~phase:LoadingPrelude)
           Stm.new_doc
           Stm.{ doc_type = VoDoc long_f_dot_vo;
-                allow_coq_overwrite = opts.boot;
                 iload_path; require_libs; stm_options;
               } in
       let state = { doc; sid; proof = None; time = opts.time } in
@@ -163,7 +162,6 @@ let compile opts copts ~echo ~f_in ~f_out =
       let doc, sid = Topfmt.(in_phase ~phase:LoadingPrelude)
           Stm.new_doc
           Stm.{ doc_type = VioDoc long_f_dot_vio;
-                allow_coq_overwrite = opts.boot;
                 iload_path; require_libs; stm_options;
               } in
 
diff --git a/toplevel/coqargs.ml b/toplevel/coqargs.ml
index 0c9201c3a5..abfda07426 100644
--- a/toplevel/coqargs.ml
+++ b/toplevel/coqargs.ml
@@ -40,8 +40,6 @@ type native_compiler = NativeOff | NativeOn of { ondemand : bool }
 
 type t = {
 
-  boot : bool;
-
   load_init   : bool;
   load_rcfile : bool;
   rcfile      : string option;
@@ -93,8 +91,6 @@ let default_native =
 
 let default = {
 
-  boot = false;
-
   load_init   = true;
   load_rcfile = true;
   rcfile      = None;
@@ -179,6 +175,10 @@ 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 }
@@ -459,7 +459,9 @@ let parse_args ~help ~init arglist : t * string list =
       { oval with batch = true }
     |"-test-mode" -> Flags.test_mode := true; oval
     |"-beautify" -> Flags.beautify := true; oval
-    |"-boot" -> { oval with boot = true; load_rcfile = false; }
+    |"-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/coqargs.mli b/toplevel/coqargs.mli
index 9cc846edea..b89a88d1f6 100644
--- a/toplevel/coqargs.mli
+++ b/toplevel/coqargs.mli
@@ -16,8 +16,6 @@ type native_compiler = NativeOff | NativeOn of { ondemand : bool }
 
 type t = {
 
-  boot : bool;
-
   load_init   : bool;
   load_rcfile : bool;
   rcfile      : string option;
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 9115fbb726..92ac200bc0 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -221,7 +221,6 @@ let init_toploop opts =
   let doc, sid =
     Stm.(new_doc
            { doc_type = Interactive opts.toplevel_name;
-             allow_coq_overwrite = true; (* irrelevant *)
              iload_path; require_libs; stm_options;
            }) in
   let state = { doc; sid; proof = None; time = opts.time } in
diff --git a/toplevel/usage.ml b/toplevel/usage.ml
index 0d17218a56..94ec6bb70d 100644
--- a/toplevel/usage.ml
+++ b/toplevel/usage.ml
@@ -62,7 +62,6 @@ let print_usage_common co command =
 \n\
 \n  -q                     skip loading of rcfile\
 \n  -init-file f           set the rcfile to f\
-\n  -boot                  boot mode (allows to overload the `Coq` library prefix, implies -q)\
 \n  -bt                    print backtraces (requires configure debug flag)\
 \n  -debug                 debug mode (implies -bt)\
 \n  -diffs (on|off|removed) highlight differences between proof steps\
-- 
cgit v1.2.3