3 files changed, 3 insertions, 30 deletions
diff --git a/library/goptions.ml b/library/goptions.ml
index dcbc46ab72..154b863fa1 100644
--- a/library/goptions.ml
+++ b/library/goptions.ml
@@ -73,7 +73,7 @@ module MakeTable =
 
     let _ =
       if String.List.mem_assoc nick !A.table then
-	user_err Pp.(str "Sorry, this table name is already used.")
+        user_err Pp.(str "Sorry, this table name (" ++ str nick ++ str ") is already used.")
 
     module MySet = Set.Make (struct type t = A.t let compare = A.compare end)
 
@@ -216,11 +216,11 @@ let get_option key = OptionMap.find key !value_tab
 
 let check_key key = try
   let _ = get_option key in
-  user_err Pp.(str "Sorry, this option name is already used.")
+  user_err Pp.(str "Sorry, this option name ("++ str (nickname key) ++ str ") is already used.")
 with Not_found ->
   if String.List.mem_assoc (nickname key) !string_table
     || String.List.mem_assoc (nickname key) !ref_table
-  then user_err Pp.(str "Sorry, this option name is already used.")
+  then user_err Pp.(str "Sorry, this option name (" ++ str (nickname key) ++ str ") is already used.")
 
 open Libobject
 
diff --git a/library/library.ml b/library/library.ml
index 0ff82d7cc4..9b9bd07c93 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -611,28 +611,6 @@ let import_module export modl =
 (************************************************************************)
 (*s Initializing the compilation of a library. *)
 
-let check_coq_overwriting p id =
-  let l = DirPath.repr p in
-  let is_empty = match l with [] -> true | _ -> false in
-  if not !Flags.boot && not is_empty && Id.equal (List.last l) coq_root then
-    user_err 
-      (str "Cannot build module " ++ DirPath.print p ++ str "." ++ Id.print id ++ str "." ++ spc () ++
-      str "it starts with prefix \"Coq\" which is reserved for the Coq library.")
-
-let start_library fo =
-  let ldir0 =
-    try
-      let lp = Loadpath.find_load_path (Filename.dirname fo) in
-      Loadpath.logical lp
-    with Not_found -> Libnames.default_root_prefix
-  in
-  let file = Filename.chop_extension (Filename.basename fo) in
-  let id = Id.of_string file in
-  check_coq_overwriting ldir0 id;
-  let ldir = add_dirpath_suffix ldir0 id in
-  Declaremods.start_library ldir;
-  ldir
-
 let load_library_todo f =
   let longf = Loadpath.locate_file (f^".v") in
   let f = longf^"io" in
diff --git a/library/library.mli b/library/library.mli
index d5815afc40..d298a371b5 100644
--- a/library/library.mli
+++ b/library/library.mli
@@ -38,11 +38,6 @@ type seg_proofs = Constr.constr Future.computation array
    an export otherwise just a simple import *)
 val import_module : bool -> qualid list -> unit
 
-(** Start the compilation of a file as a library. The first argument must be
-    output file, and the 
-    returned path is the associated absolute logical path of the library. *)
-val start_library : CUnix.physical_path -> DirPath.t
-
 (** End the compilation of a library and save it to a ".vo" file *)
 val save_library_to :
   ?todo:(((Future.UUID.t,'document) Stateid.request * bool) list * 'counters) ->