5 files changed, 15 insertions, 12 deletions

diff --git a/library/declare.ml b/library/declare.ml
index 3a640c971..906d9aa3c 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -112,11 +112,17 @@ let open_constant i ((sp,kn),_) =
   let con = Global.constant_of_delta (constant_of_kn kn) in
     Nametab.push (Nametab.Exactly i) sp (ConstRef con)
 
+let exists_name id =
+  variable_exists id or Global.exists_label (label_of_id id)
+
+let check_exists sp =
+  let id = basename sp in
+  if exists_name id then alreadydeclared (pr_id id ++ str " already exists")
+
 let cache_constant ((sp,kn),(cdt,dhyps,kind)) =
   let id = basename sp in
   let _,dir,_ = repr_kn kn in
-  if variable_exists id or Nametab.exists_cci sp then
-    alreadydeclared (pr_id id ++ str " already exists");
+  check_exists sp;
   let kn' = Global.add_constant dir id cdt in
   assert (kn' = constant_of_kn kn);
   Nametab.push (Nametab.Until 1) sp (ConstRef (constant_of_kn kn));
@@ -197,16 +203,8 @@ let inductive_names sp kn mie =
       ([], 0) mie.mind_entry_inds
   in names
 
-let check_exists_inductive (sp,_) =
-  (if variable_exists (basename sp) then
-    alreadydeclared (pr_id (basename sp) ++ str " already exists"));
-  if Nametab.exists_cci sp then
-    let (_,id) = repr_path sp in
-    alreadydeclared (pr_id id ++ str " already exists")
-
 let load_inductive i ((sp,kn),(_,mie)) =
   let names = inductive_names sp kn mie in
-  List.iter check_exists_inductive names;
   List.iter (fun (sp, ref) -> Nametab.push (Nametab.Until i) sp ref ) names
 
 let open_inductive i ((sp,kn),(_,mie)) =
@@ -215,7 +213,7 @@ let open_inductive i ((sp,kn),(_,mie)) =
 
 let cache_inductive ((sp,kn),(dhyps,mie)) =
   let names = inductive_names sp kn mie in
-  List.iter check_exists_inductive names;
+  List.iter check_exists (List.map fst names);
   let id = basename sp in
   let _,dir,_ = repr_kn kn in
   let kn' = Global.add_mind dir id mie in
diff --git a/library/declare.mli b/library/declare.mli
index 1ad733816..61c199960 100644
--- a/library/declare.mli
+++ b/library/declare.mli
@@ -79,3 +79,4 @@ val cofixpoint_message : identifier list -> unit
 val recursive_message : bool (** true = fixpoint *) ->
   int array option -> identifier list -> unit
 
+val exists_name : identifier -> bool
diff --git a/library/global.ml b/library/global.ml
index dfcd8c410..6548e6537 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -128,7 +128,9 @@ let mind_of_delta mind =
   let resolver,resolver_param = (delta_of_senv !global_env) in
     Mod_subst.mind_of_delta resolver_param
       (Mod_subst.mind_of_delta resolver mind)
-	
+
+let exists_label id = exists_label id !global_env
+
 let start_library dir =
   let mp,newenv = start_library dir !global_env in
     global_env := newenv;
diff --git a/library/global.mli b/library/global.mli
index 9beb535d5..7859c51ef 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -87,6 +87,7 @@ val lookup_module    : module_path -> module_body
 val lookup_modtype   : module_path -> module_type_body
 val constant_of_delta : constant -> constant
 val mind_of_delta : mutual_inductive -> mutual_inductive
+val exists_label     : label -> bool
 
 (** Compiled modules *)
 val start_library : dir_path -> module_path
diff --git a/library/libnames.ml b/library/libnames.ml
index c82b3476e..b91d24bd6 100644
--- a/library/libnames.ml
+++ b/library/libnames.ml
@@ -195,6 +195,7 @@ type full_path = {
   basename : identifier }
 
 let make_path pa id = { dirpath = pa; basename = id }
+
 let repr_path { dirpath = pa; basename = id } = (pa,id)
 
 (* parsing and printing of section paths *)