Make boot flag into a normal option (no global flag).

5 files changed, 15 insertions, 6 deletions

diff --git a/toplevel/ccompile.ml b/toplevel/ccompile.ml
index df2b983029..ecb0407f75 100644
--- a/toplevel/ccompile.ml
+++ b/toplevel/ccompile.ml
@@ -109,6 +109,7 @@ 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
@@ -159,6 +160,7 @@ 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 74c016101a..ae3c5b32dc 100644
--- a/toplevel/coqargs.ml
+++ b/toplevel/coqargs.ml
@@ -35,6 +35,8 @@ type color = [`ON | `AUTO | `OFF]
 
 type t = {
 
+  boot : bool;
+
   load_init   : bool;
   load_rcfile : bool;
   rcfile      : string option;
@@ -81,6 +83,8 @@ let default_toplevel = Names.(DirPath.make [Id.of_string "Top"])
 
 let default = {
 
+  boot = false;
+
   load_init   = true;
   load_rcfile = true;
   rcfile      = None;
@@ -232,9 +236,9 @@ let usage_no_coqlib = CWarnings.create ~name:"usage-no-coqlib" ~category:"filesy
 
 exception NoCoqLib
 
-let usage help =
+let usage ~boot help =
   begin
-    try Envars.set_coqlib ~fail:(fun x -> raise NoCoqLib)
+    try Envars.set_coqlib ~boot ~fail:(fun x -> raise NoCoqLib)
     with NoCoqLib -> usage_no_coqlib ()
   end;
   let lp = Coqinit.toplevel_init_load_path () in
@@ -436,7 +440,7 @@ 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" -> Flags.boot := true; { oval with load_rcfile = false; }
+    |"-boot" -> { oval with boot = true; load_rcfile = false; }
     |"-bt" -> Backtrace.record_backtrace true; oval
     |"-color" -> set_color oval (next ())
     |"-config"|"--config" -> { oval with print_config = true }
@@ -468,7 +472,7 @@ let parse_args ~help ~init arglist : t * string list =
     |"-type-in-type" -> set_type_in_type (); oval
     |"-unicode" -> add_vo_require oval "Utf8_core" None (Some false)
     |"-where" -> { oval with print_where = true }
-    |"-h"|"-H"|"-?"|"-help"|"--help" -> usage help; oval
+    |"-h"|"-H"|"-?"|"-help"|"--help" -> usage ~boot:oval.boot help; oval
     |"-v"|"--version" -> Usage.version (exitcode oval)
     |"-print-version"|"--print-version" ->
       Usage.machine_readable_version (exitcode oval)
diff --git a/toplevel/coqargs.mli b/toplevel/coqargs.mli
index c9a7a0fd56..52ab2b60d7 100644
--- a/toplevel/coqargs.mli
+++ b/toplevel/coqargs.mli
@@ -14,6 +14,8 @@ val default_toplevel : Names.DirPath.t
 
 type t = {
 
+  boot : bool;
+
   load_init   : bool;
   load_rcfile : bool;
   rcfile      : string option;
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 6ef0aa390d..faf26a9665 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -162,7 +162,7 @@ let init_toplevel ~help ~init custom_init arglist =
   (* If we have been spawned by the Spawn module, this has to be done
    * early since the master waits us to connect back *)
   Spawned.init_channels ();
-  Envars.set_coqlib ~fail:(fun msg -> CErrors.user_err Pp.(str msg));
+  Envars.set_coqlib ~boot:opts.boot ~fail:(fun msg -> CErrors.user_err Pp.(str msg));
   if opts.print_where then begin
     print_endline (Envars.coqlib ());
     exit (exitcode opts)
@@ -221,6 +221,7 @@ 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 277f8b7367..0d17218a56 100644
--- a/toplevel/usage.ml
+++ b/toplevel/usage.ml
@@ -62,7 +62,7 @@ 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)\
+\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\