Merge PR #11617: [init] Add `-boot` option to avoid binding `Coq.` prefix.

Reviewed-by: SkySkimmer
Ack-by: Zimmi48
Reviewed-by: herbelin

6 files changed, 17 insertions, 7 deletions

diff --git a/doc/changelog/07-commands-and-options/11617-toplevel+boot.rst b/doc/changelog/07-commands-and-options/11617-toplevel+boot.rst
new file mode 100644
index 0000000000..49dd0ee2d8
--- /dev/null
+++ b/doc/changelog/07-commands-and-options/11617-toplevel+boot.rst
@@ -0,0 +1,5 @@
+- **Added:**
+  New ``coqc`` / ``coqtop`` option ``-boot`` that will not bind the
+  `Coq` library prefix by default
+  (`#11617 <https://github.com/coq/coq/pull/11617>`_,
+  by Emilio Jesus Gallego Arias).
diff --git a/toplevel/coqargs.ml b/toplevel/coqargs.ml
index 506a8dc5b0..2b79bff1b2 100644
--- a/toplevel/coqargs.ml
+++ b/toplevel/coqargs.ml
@@ -64,6 +64,7 @@ type coqargs_config = {
 }
 
 type coqargs_pre = {
+  boot        : bool;
   load_init   : bool;
   load_rcfile : bool;
 
@@ -131,6 +132,7 @@ let default_config = {
 }
 
 let default_pre = {
+  boot         = false;
   load_init    = true;
   load_rcfile  = true;
   ml_includes  = [];
@@ -512,6 +514,7 @@ let parse_args ~help ~init arglist : t * string list =
     |"-indices-matter" -> set_logic (fun o -> { o with indices_matter = true }) oval
     |"-m"|"--memory" -> { oval with post = { oval.post with memory_stat = true }}
     |"-noinit"|"-nois" -> { oval with pre = { oval.pre with load_init = false }}
+    |"-boot" -> { oval with pre = { oval.pre with boot = true }}
     |"-output-context" -> { oval with post = { oval.post with output_context = true }}
     |"-profile-ltac" -> Flags.profile_ltac := true; oval
     |"-q" -> { oval with pre = { oval.pre with load_rcfile = false; }}
@@ -569,5 +572,5 @@ let cmdline_load_path opts =
   opts.pre.ml_includes @ opts.pre.vo_includes
 
 let build_load_path opts =
-  Coqinit.libs_init_load_path ~load_init:opts.pre.load_init @
+  (if opts.pre.boot then [] else Coqinit.libs_init_load_path ()) @
   cmdline_load_path opts
diff --git a/toplevel/coqargs.mli b/toplevel/coqargs.mli
index 26f22386a0..f38381a086 100644
--- a/toplevel/coqargs.mli
+++ b/toplevel/coqargs.mli
@@ -40,6 +40,7 @@ type coqargs_config = {
 }
 
 type coqargs_pre = {
+  boot        : bool;
   load_init   : bool;
   load_rcfile : bool;
 
diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml
index 3aa9acfc52..7f3d4b570f 100644
--- a/toplevel/coqinit.ml
+++ b/toplevel/coqinit.ml
@@ -52,10 +52,10 @@ let load_rcfile ~rcfile ~state =
       iraise reraise
 
 (* Recursively puts `.v` files in the LoadPath if -nois was not passed *)
-let build_stdlib_vo_path ~load_init ~unix_path ~coq_path =
+let build_stdlib_vo_path ~unix_path ~coq_path =
   let open Loadpath in
   { recursive = true;
-    path_spec = VoPath { unix_path; coq_path ; has_ml = AddNoML; implicit = load_init }
+    path_spec = VoPath { unix_path; coq_path ; has_ml = AddNoML; implicit = true }
   }
 
 let build_stdlib_ml_path ~dir =
@@ -88,7 +88,7 @@ let toplevel_init_load_path () =
   ml_path_if Coq_config.local [coqlib/"dev"]
 
 (* LoadPath for Coq user libraries *)
-let libs_init_load_path ~load_init =
+let libs_init_load_path () =
 
   let open Loadpath in
   let coqlib = Envars.coqlib () in
@@ -107,7 +107,7 @@ let libs_init_load_path ~load_init =
 
   (* then standard library *)
   [build_stdlib_ml_path ~dir:(coqlib/"plugins")] @
-  [build_stdlib_vo_path ~load_init ~unix_path:(coqlib/"theories") ~coq_path] @
+  [build_stdlib_vo_path ~unix_path:(coqlib/"theories") ~coq_path] @
 
   (* then user-contrib *)
   (if Sys.file_exists user_contrib then
diff --git a/toplevel/coqinit.mli b/toplevel/coqinit.mli
index fc53c8b47c..f3a007d987 100644
--- a/toplevel/coqinit.mli
+++ b/toplevel/coqinit.mli
@@ -20,4 +20,4 @@ val init_ocaml_path : unit -> unit
 val toplevel_init_load_path : unit -> Loadpath.coq_path list
 
 (* LoadPath for Coq user libraries *)
-val libs_init_load_path : load_init:bool -> Loadpath.coq_path list
+val libs_init_load_path : unit -> Loadpath.coq_path list
diff --git a/toplevel/usage.ml b/toplevel/usage.ml
index 6848862603..ba3deeb2f6 100644
--- a/toplevel/usage.ml
+++ b/toplevel/usage.ml
@@ -32,7 +32,8 @@ let print_usage_common co command =
 \n  -coqlib dir            set the coq standard library directory\
 \n  -exclude-dir f         exclude subdirectories named f for option -R\
 \n\
-\n  -noinit                start without loading the Init library\
+\n  -boot                  don't bind the `Coq.` prefix to the default -coqlib dir\
+\n  -noinit                don't load Coq.Init.Prelude on start \
 \n  -nois                  (idem)\
 \n  -compat X.Y            provides compatibility support for Coq version X.Y\
 \n\