diff options
Diffstat (limited to 'stm')
| -rw-r--r-- | stm/stm.ml | 15 | ||||
| -rw-r--r-- | stm/stm.mli | 4 |
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; |