From 4a3450a90d1037340acddccdc9e462bed5bd2164 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 1 Jul 2009 11:58:59 +0000
Subject: 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
---
 library/library.ml  | 8 +++++---
 library/library.mli | 3 ---
 2 files changed, 5 insertions(+), 6 deletions(-)

(limited to 'library')

diff --git a/library/library.ml b/library/library.ml
index c812819a24..abca3c7e75 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 2b7ecc6648..c6bd8fe0b7 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
-- 
cgit v1.2.3