Merge PR #9523: Make boot flag into a normal option (no global flag).

Ack-by: SkySkimmer
Reviewed-by: ejgallego

2 files changed, 14 insertions, 5 deletions

diff --git a/stm/stm.ml b/stm/stm.ml
index f6b4593087..e7833f253e 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -2647,6 +2647,10 @@ type stm_init_options = {
      some point. *)
   doc_type     : stm_doc_type;
 
+  (* Allow compiling modules in the Coq prefix. Irrelevant in
+     interactive mode. *)
+  allow_coq_overwrite : bool;
+
   (* Initial load path in scope for the document. Usually extracted
      from -R options / _CoqProject *)
   iload_path   : Mltop.coq_path list;
@@ -2674,11 +2678,12 @@ let init_core () =
   if !cur_opt.async_proofs_mode = APon then Control.enable_thread_delay := true;
   State.register_root_state ()
 
-let check_coq_overwriting p =
+let check_coq_overwriting ~allow_coq_overwrite p =
+  if not allow_coq_overwrite then
   let l = DirPath.repr p in
   let id, l = match l with id::l -> id,l | [] -> assert false in
   let is_empty = match l with [] -> true | _ -> false in
-  if not !Flags.boot && not is_empty && Id.equal (CList.last l) Libnames.coq_root then
+  if not is_empty && Id.equal (CList.last l) Libnames.coq_root then
     user_err
       (str "Cannot build module " ++ DirPath.print p ++ str "." ++ spc () ++
       str "it starts with prefix \"Coq\" which is reserved for the Coq library.")
@@ -2695,7 +2700,7 @@ let dirpath_of_file f =
   let ldir = Libnames.add_dirpath_suffix ldir0 id in
   ldir
 
-let new_doc { doc_type ; iload_path; require_libs; stm_options } =
+let new_doc { doc_type ; allow_coq_overwrite; iload_path; require_libs; stm_options } =
 
   let load_objs libs =
     let rq_file (dir, from, exp) =
@@ -2730,14 +2735,14 @@ let new_doc { doc_type ; iload_path; require_libs; stm_options } =
 
     | VoDoc f ->
       let ldir = dirpath_of_file f in
-      check_coq_overwriting ldir;
+      check_coq_overwriting ~allow_coq_overwrite ldir;
       let () = Flags.verbosely Declaremods.start_library ldir in
       VCS.set_ldir ldir;
       set_compilation_hints f
 
     | VioDoc f ->
       let ldir = dirpath_of_file f in
-      check_coq_overwriting ldir;
+      check_coq_overwriting ~allow_coq_overwrite ldir;
       let () = Flags.verbosely Declaremods.start_library ldir in
       VCS.set_ldir ldir;
       set_compilation_hints f
diff --git a/stm/stm.mli b/stm/stm.mli
index 821ab59a43..313ac58111 100644
--- a/stm/stm.mli
+++ b/stm/stm.mli
@@ -67,6 +67,10 @@ type stm_init_options = {
      some point. *)
   doc_type     : stm_doc_type;
 
+  (* Allow compiling modules in the Coq prefix. Irrelevant in
+     interactive mode. *)
+  allow_coq_overwrite : bool;
+
   (* Initial load path in scope for the document. Usually extracted
      from -R options / _CoqProject *)
   iload_path   : Mltop.coq_path list;