Support for binding Coq root read-only in -R option

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12220 85f007b7-540e-0410-9357-904b9bb8a0f7

2 files changed, 5 insertions, 6 deletions

diff --git a/library/library.ml b/library/library.ml
index c812819a2..abca3c7e7 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -601,18 +601,20 @@ let import_module export (loc,qid) =
 (************************************************************************)
 (*s Initializing the compilation of a library. *)
 
-let check_coq_overwriting p =
+let check_coq_overwriting p id =
   let l = repr_dirpath p in
   if not !Flags.boot && l <> [] && string_of_id (list_last l) = "Coq" then
-    errorlabstrm "" (strbrk ("Name "^string_of_dirpath p^" starts with prefix \"Coq\" which is reserved for the Coq library."))
+    errorlabstrm ""
+      (strbrk ("Cannot build module "^string_of_dirpath p^"."^string_of_id id^
+      ": it starts with prefix \"Coq\" which is reserved for the Coq library."))
 
 let start_library f = 
   let paths = get_load_paths () in
   let _,longf =
     System.find_file_in_path ~warn:(Flags.is_verbose()) paths (f^".v") in
   let ldir0 = find_logical_path (Filename.dirname longf) in
-  check_coq_overwriting ldir0;
   let id = id_of_string (Filename.basename f) in
+  check_coq_overwriting ldir0 id;
   let ldir = extend_dirpath ldir0 id in
   Declaremods.start_library ldir;
   ldir,longf
diff --git a/library/library.mli b/library/library.mli
index 2b7ecc664..c6bd8fe0b 100644
--- a/library/library.mli
+++ b/library/library.mli
@@ -79,8 +79,5 @@ val locate_qualified_library :
   bool -> qualid -> library_location * dir_path * System.physical_path
 val try_locate_qualified_library : qualid located -> dir_path * string
 
-(* Reserve Coq prefix for the standard library *)
-val check_coq_overwriting : dir_path -> unit
-
 (*s Statistics: display the memory use of a library. *)
 val mem : dir_path -> Pp.std_ppcmds