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, 12 insertions, 10 deletions

diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index b8fe1571c..0e5af7737 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -89,9 +89,6 @@ type module_info =
      variant : modvariant;
      resolver : delta_resolver;
      resolver_of_param : delta_resolver;}
-      
-let check_label l labset =
-  if Labset.mem l labset then error_existing_label l
 
 let set_engagement_opt oeng env =
   match oeng with
@@ -112,6 +109,11 @@ type safe_environment =
       loads : (module_path * module_body) list;
       local_retroknowledge : Retroknowledge.action list}
 
+let exists_label l senv = Labset.mem l senv.labset
+
+let check_label l senv =
+  if exists_label l senv then error_existing_label l
+
 (* a small hack to avoid variants and an unused case in all functions *)
 let rec empty_environment =
   { old = empty_environment;
@@ -276,7 +278,7 @@ let hcons_constant_body cb =
     const_type = hcons_const_type cb.const_type }
 
 let add_constant dir l decl senv =
-  check_label l senv.labset;
+  check_label l senv;
   let kn = make_con senv.modinfo.modpath dir l in
   let cb =
     match decl with
@@ -303,7 +305,7 @@ let add_mind dir l mie senv =
   if l <> label_of_id id then
     anomaly ("the label of inductive packet and its first inductive"^
 	     " type do not match");
-  check_label l senv.labset;
+  check_label l senv;
     (* TODO: when we will allow reorderings we will have to verify
        all labels *)
   let kn = make_mind senv.modinfo.modpath dir l in
@@ -314,7 +316,7 @@ let add_mind dir l mie senv =
 (* Insertion of module types *)
 
 let add_modtype l mte inl senv =
-  check_label l senv.labset;
+  check_label l senv;
   let mp = MPdot(senv.modinfo.modpath, l) in
   let mtb = translate_module_type senv.env mp inl mte  in
   let senv' = add_field (l,SFBmodtype mtb) (MT mp) senv in
@@ -328,7 +330,7 @@ let full_add_module mb senv =
 (* Insertion of modules *)
 
 let add_module l me inl senv =
-  check_label l senv.labset;
+  check_label l senv;
   let mp = MPdot(senv.modinfo.modpath, l) in
   let mb = translate_module senv.env mp inl me in
   let senv' = add_field (l,SFBmodule mb) M senv in
@@ -341,7 +343,7 @@ let add_module l me inl senv =
 (* Interactive modules *)
 
 let start_module l senv =
-  check_label l senv.labset;
+  check_label l senv;
  let mp = MPdot(senv.modinfo.modpath, l) in
  let modinfo = { modpath = mp;
 		 label = l;
@@ -491,7 +493,7 @@ let end_module l restype senv =
    let senv = update_resolver (add_delta_resolver resolver) senv
    in
    let add senv ((l,elem) as field) =
-     check_label l senv.labset;
+     check_label l senv;
      let new_name = match elem with
        | SFBconst _ ->
 	   let kn = make_kn mp_sup empty_dirpath l in
@@ -552,7 +554,7 @@ let add_module_parameter mbid mte inl senv =
 (* Interactive module types *)
 
 let start_modtype l senv =
-  check_label l senv.labset;
+  check_label l senv;
  let mp = MPdot(senv.modinfo.modpath, l) in
  let modinfo = { modpath = mp;
 		 label = l;