Rely on kernel to know if a name is already used so as to be consistent with it.

Maybe could we keep only the kernel check, but message would
certainly need to be reformulated then.

For instance, the message was previously different for an attempt to
redefine a name whether this name was in the same section or not.

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

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 *)