Module names and constant/inductive names are now in two separate namespaces

 We now accept the following code: Definition E := 0. Module E. End E.

 Techically, we simply allow the same label to occur at most twice in
 a structure_body, which is a (label * structure_field_body) list).
 These two label occurences should not be at the same level of fields
 (e.g. a SFBmodule and a SFBmind are ok, but not two SFBmodule's or
 a SFBmodule and a SFBmodtype). Gain : a minimal amount of code change.
 Drawback : no more simple List.assoc or equivalent should be performed
 on a structure_body ...

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

4 files changed, 15 insertions, 9 deletions

diff --git a/library/assumptions.ml b/library/assumptions.ml
index e047b62a6..a26dc2ca2 100644
--- a/library/assumptions.ml
+++ b/library/assumptions.ml
@@ -55,6 +55,16 @@ module ContextObjectMap = Map.Make (OrderedContextObject)
 
 let modcache = ref (MPmap.empty : structure_body MPmap.t)
 
+let rec search_mod_label lab = function
+  | [] -> raise Not_found
+  | (l,SFBmodule mb) :: _ when l = lab -> mb
+  | _ :: fields -> search_mod_label lab fields
+
+let rec search_cst_label lab = function
+  | [] -> raise Not_found
+  | (l,SFBconst cb) :: _ when l = lab -> cb
+  | _ :: fields -> search_cst_label lab fields
+
 let rec lookup_module_in_impl mp =
   try Global.lookup_module mp
   with Not_found ->
@@ -65,9 +75,7 @@ let rec lookup_module_in_impl mp =
 	raise Not_found (* should have been found by [lookup_module] *)
       | MPdot (mp',lab') ->
 	let fields = memoize_fields_of_mp mp' in
-	match List.assoc lab' fields with
-	  | SFBmodule mb -> mb
-	  | _ -> assert false (* same label for a non-module ?! *)
+	search_mod_label lab' fields
 
 and memoize_fields_of_mp mp =
   try MPmap.find mp !modcache
@@ -127,9 +135,7 @@ let lookup_constant_in_impl cst fallback =
     let fields = memoize_fields_of_mp mp in
     (* A module found this way is necessarily closed, in particular
        our constant cannot be in an opened section : *)
-    match List.assoc lab fields with
-      | SFBconst cb -> cb
-      | _ -> assert false (* label not pointing to a constant ?! *)
+    search_cst_label lab fields
   with Not_found ->
     (* Either:
        - The module part of the constant isn't registered yet :
diff --git a/library/declare.ml b/library/declare.ml
index fd3139cf6..f3df8347e 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -117,7 +117,7 @@ let open_constant i ((sp,kn),_) =
     Nametab.push (Nametab.Exactly i) sp (ConstRef con)
 
 let exists_name id =
-  variable_exists id or Global.exists_label (label_of_id id)
+  variable_exists id or Global.exists_objlabel (label_of_id id)
 
 let check_exists sp =
   let id = basename sp in
diff --git a/library/global.ml b/library/global.ml
index 926284f91..e57aea6c9 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -134,7 +134,7 @@ let mind_of_delta_kn kn =
     Mod_subst.mind_of_delta resolver_param
       (Mod_subst.mind_of_delta_kn resolver kn)
 
-let exists_label id = exists_label id !global_env
+let exists_objlabel id = exists_objlabel id !global_env
 
 let start_library dir =
   let mp,newenv = start_library dir !global_env in
diff --git a/library/global.mli b/library/global.mli
index 1a0fabdc8..77fd465c8 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -87,7 +87,7 @@ val lookup_module    : module_path -> module_body
 val lookup_modtype   : module_path -> module_type_body
 val constant_of_delta_kn : kernel_name -> constant
 val mind_of_delta_kn : kernel_name -> mutual_inductive
-val exists_label     : label -> bool
+val exists_objlabel  : label -> bool
 
 (** Compiled modules *)
 val start_library : dir_path -> module_path