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

1 files changed, 3 insertions, 1 deletions

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;