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

14 files changed, 218 insertions, 184 deletions

diff --git a/CHANGES b/CHANGES
index b38a346a0..cdcda4ed1 100644
--- a/CHANGES
+++ b/CHANGES
@@ -19,6 +19,12 @@ Program
   consistent with "Proof with".
 - Program Lemma, Definition now respect automatic introduction.
 
+Module System
+
+- The names of modules (and module types) are now in a fully separated
+  namespace from ordinary definitions : "Definition E:=0. Module E. End E."
+  is now accepted.
+
 CoqIDE
 
 - Coqide now supports the Restart command, and Undo (with a warning).
diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml
index b49db27c3..7a66ced77 100644
--- a/checker/mod_checking.ml
+++ b/checker/mod_checking.ml
@@ -54,10 +54,14 @@ let path_of_mexpr = function
   | SEBident mp -> mp
   | _ -> raise Not_path
 
-let rec list_split_assoc k rev_before = function
+let is_modular = function
+  | SFBmodule _ | SFBmodtype _ -> true
+  | SFBconst _ | SFBmind _ -> false
+
+let rec list_split_assoc ((k,m) as km) rev_before = function
   | [] -> raise Not_found
-  | (k',b)::after when k=k' -> rev_before,b,after
-  | h::tail -> list_split_assoc k (h::rev_before) tail
+  | (k',b)::after when k=k' && is_modular b = m -> rev_before,b,after
+  | h::tail -> list_split_assoc km (h::rev_before) tail
 
 let check_definition_sub env cb1 cb2 =
   let check_type env t1 t2 =
@@ -132,38 +136,35 @@ let lookup_modtype mp env =
 
 let rec check_with env mtb with_decl mp=
   match with_decl with
-    | With_definition_body _ ->
-	check_with_aux_def env mtb with_decl mp;
+    | With_definition_body (idl,c) ->
+	check_with_def env mtb (idl,c) mp;
 	mtb
-    | With_module_body _ ->
-	check_with_aux_mod env mtb with_decl mp;
+    | With_module_body (idl,mp1) ->
+	check_with_mod env mtb (idl,mp1) mp;
 	mtb
 
-and check_with_aux_def env mtb with_decl mp =
+and check_with_def env mtb (idl,c) mp =
   let sig_b = match mtb with
     | SEBstruct(sig_b) ->
 	sig_b
     | _ -> error_signature_expected mtb
   in
-  let id,idl = match with_decl with
-    | With_definition_body (id::idl,_) | With_module_body (id::idl,_) ->
-                                           id,idl
-    | With_definition_body ([],_) | With_module_body ([],_) -> assert false
+  let id,idl = match idl with
+    | [] -> assert false
+    | id::idl -> id,idl
   in
   let l = label_of_id id in
     try
-      let rev_before,spec,after = list_split_assoc l [] sig_b in
+      let rev_before,spec,after = list_split_assoc (l,(idl<>[])) [] sig_b in
       let before = List.rev rev_before in
       let env' = Modops.add_signature mp before empty_delta_resolver env in
-	match with_decl with
-          | With_definition_body ([],_) -> assert false
-	  | With_definition_body ([id],c) ->
+      if idl = [] then
 	      let cb = match spec with
 		  SFBconst cb -> cb
 		| _ -> error_not_a_constant l
 	      in
               check_definition_sub env' c cb
-	  | With_definition_body (_::_,_) ->
+      else
 	      let old = match spec with
 		  SFBmodule msb -> msb
 		| _ -> error_not_a_module l
@@ -171,49 +172,36 @@ and check_with_aux_def env mtb with_decl mp =
 		begin
 		  match old.mod_expr with
                     | None ->
-			let new_with_decl = match with_decl with
-			    With_definition_body (_,c) ->
-                              With_definition_body (idl,c)
-			  | With_module_body (_,c) ->
-                              With_module_body (idl,c) in
-			  check_with_aux_def env' old.mod_type new_with_decl (MPdot(mp,l))
+		        check_with_def env' old.mod_type (idl,c) (MPdot(mp,l))
                     | Some msb ->
 			error_a_generative_module_expected l
 		end
-	  | _ -> anomaly "Modtyping:incorrect use of with"
     with
 	Not_found -> error_no_such_label l
       | Reduction.NotConvertible -> error_with_incorrect l
 
-and check_with_aux_mod env mtb with_decl mp =
+and check_with_mod env mtb (idl,mp1) mp =
   let sig_b =
     match mtb with
     | SEBstruct(sig_b) ->
 	sig_b
     | _ -> error_signature_expected mtb in
-  let id,idl = match with_decl with
-    | With_definition_body (id::idl,_) | With_module_body (id::idl,_) ->
-        id,idl
-    | With_definition_body ([],_) | With_module_body ([],_) -> assert false
+  let id,idl = match idl with
+    | [] -> assert false
+    | id::idl -> id,idl
   in
   let l = label_of_id id in
     try
-      let rev_before,spec,after = list_split_assoc l [] sig_b in
+      let rev_before,spec,after = list_split_assoc (l,false) [] sig_b in
       let before = List.rev rev_before in
-      let rec mp_rec = function
-	| [] -> mp
-	| i::r -> MPdot(mp_rec r,label_of_id i)
-      in
       let env' = Modops.add_signature mp before empty_delta_resolver env in
-	match with_decl with
-          | With_module_body ([],_) -> assert false
-	  | With_module_body ([id], mp1) ->
+      if idl = [] then
 	      let _ = match spec with
 		  SFBmodule msb -> msb
 		| _ -> error_not_a_module l
 	      in
 	      let (_:module_body) = (lookup_module mp1 env) in ()
-        | With_module_body (_::_,mp) ->
+      else
 	    let old = match spec with
 		SFBmodule msb -> msb
 	      | _ -> error_not_a_module l
@@ -221,17 +209,11 @@ and check_with_aux_mod env mtb with_decl mp =
 	      begin
 		match old.mod_expr with
                     None ->
-                      let new_with_decl = match with_decl with
-			  With_definition_body (_,c) ->
-			    With_definition_body (idl,c)
-			| With_module_body (_,c) ->
-                            With_module_body (idl,c) in
-		 	check_with_aux_mod env'
-			  old.mod_type new_with_decl (MPdot(mp,l))
+		      check_with_mod env'
+			  old.mod_type (idl,mp1) (MPdot(mp,l))
                   | Some msb ->
                       error_a_generative_module_expected l
               end
-	| _ -> anomaly "Modtyping:incorrect use of with"
     with
 	Not_found -> error_no_such_label l
       | Reduction.NotConvertible -> error_with_incorrect l
diff --git a/checker/subtyping.ml b/checker/subtyping.ml
index 8fb4eb34b..3da7bd0e2 100644
--- a/checker/subtyping.ml
+++ b/checker/subtyping.ml
@@ -29,15 +29,18 @@ type namedobject =
   | Constant of constant_body
   | IndType of inductive * mutual_inductive_body
   | IndConstr of constructor * mutual_inductive_body
+
+type namedmodule =
   | Module of module_body
   | Modtype of module_type_body
 
 (* adds above information about one mutual inductive: all types and
    constructors *)
 
-let add_nameobjects_of_mib ln mib map =
-  let add_nameobjects_of_one j oib map =
-    let ip = (ln,j) in
+let add_mib_nameobjects mp l mib map =
+  let ind = make_mind mp empty_dirpath l in
+  let add_mip_nameobjects j oib map =
+    let ip = (ind,j) in
     let map =
       array_fold_right_i
       (fun i id map ->
@@ -47,22 +50,32 @@ let add_nameobjects_of_mib ln mib map =
     in
       Labmap.add (label_of_id oib.mind_typename) (IndType (ip, mib)) map
   in
-    array_fold_right_i add_nameobjects_of_one mib.mind_packets map
+    array_fold_right_i add_mip_nameobjects mib.mind_packets map
+
+
+(* creates (namedobject/namedmodule) map for the whole signature *)
 
+type labmap = { objs : namedobject Labmap.t; mods : namedmodule Labmap.t }
 
-(* creates namedobject map for the whole signature *)
+let empty_labmap = { objs = Labmap.empty; mods = Labmap.empty }
 
-let make_label_map mp list =
+let get_obj mp map l =
+  try Labmap.find l map.objs
+  with Not_found -> error_no_such_label_sub l mp
+
+let get_mod mp map l =
+  try Labmap.find l map.mods
+  with Not_found -> error_no_such_label_sub l mp
+
+let make_labmap mp list =
   let add_one (l,e) map =
-   let add_map obj = Labmap.add l obj map in
    match e with
-    | SFBconst cb -> add_map (Constant cb)
-    | SFBmind mib ->
-       add_nameobjects_of_mib (make_mind mp empty_dirpath l) mib map
-    | SFBmodule mb -> add_map (Module mb)
-    | SFBmodtype mtb -> add_map (Modtype mtb)
+    | SFBconst cb -> { map with objs = Labmap.add l (Constant cb) map.objs }
+    | SFBmind mib -> { map with objs = add_mib_nameobjects mp l mib map.objs }
+    | SFBmodule mb -> { map with mods = Labmap.add l (Module mb) map.mods }
+    | SFBmodtype mtb -> { map with mods = Labmap.add l (Modtype mtb) map.mods }
   in
-    List.fold_right add_one list Labmap.empty
+  List.fold_right add_one list empty_labmap
 
 
 let check_conv_error error f env a1 a2 =
@@ -283,7 +296,6 @@ let check_constant env mp1 l info1 cb2 spec2 subst1 subst2 =
       let ty1 = type_of_constructor cstr (mind1,mind1.mind_packets.(i)) in
       let ty2 = Typeops.type_of_constant_type env cb2.const_type in
        check_conv conv env ty1 ty2
-   | _ -> error ()
 
 let rec check_modules  env msb1 msb2 subst1 subst2 =
   let mty1 = module_type_of_module None msb1 in
@@ -292,29 +304,25 @@ let rec check_modules  env msb1 msb2 subst1 subst2 =
  
 
 and check_signatures env mp1 sig1 sig2 subst1 subst2 = 
-  let map1 = make_label_map mp1 sig1 in
+  let map1 = make_labmap mp1 sig1 in
   let check_one_body  (l,spec2) =
-    let info1 =
-      try
-	Labmap.find l map1
-      with
-	  Not_found -> error_no_such_label_sub l mp1
-    in
       match spec2 with
 	| SFBconst cb2 ->
-	    check_constant  env mp1 l info1 cb2 spec2 subst1 subst2
+	    check_constant  env mp1 l (get_obj mp1 map1 l)
+	      cb2 spec2 subst1 subst2
 	| SFBmind mib2 ->
-	    check_inductive env mp1 l info1 mib2 spec2 subst1 subst2
+	    check_inductive env mp1 l (get_obj mp1 map1 l)
+	      mib2 spec2 subst1 subst2
 	| SFBmodule msb2 ->
 	    begin
-	      match info1 with
+	      match get_mod mp1 map1 l with
 		| Module msb -> check_modules env msb msb2 
 		    subst1 subst2
 		| _ -> error_not_match l spec2
 	    end
 	| SFBmodtype mtb2 ->
 	    let mtb1 =
-	      match info1 with
+	      match get_mod mp1 map1 l with
 		| Modtype mtb -> mtb
 		| _ -> error_not_match l spec2
 	    in
diff --git a/kernel/declarations.mli b/kernel/declarations.mli
index 5b800edec..7cf74ba3c 100644
--- a/kernel/declarations.mli
+++ b/kernel/declarations.mli
@@ -192,6 +192,10 @@ type structure_field_body =
   | SFBmodule of module_body
   | SFBmodtype of module_type_body
 
+(** NB: we may encounter now (at most) twice the same label in
+    a [structure_body], once for a module ([SFBmodule] or [SFBmodtype])
+    and once for an object ([SFBconst] or [SFBmind]) *)
+
 and structure_body = (label * structure_field_body) list
 
 and struct_expr_body =
diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml
index e2304f119..4cb6fc2fd 100644
--- a/kernel/mod_typing.ml
+++ b/kernel/mod_typing.ml
@@ -36,10 +36,14 @@ let rec mp_from_mexpr = function
   | MSEfunctor (_,_,expr) -> mp_from_mexpr expr
   | MSEwith (expr,_) -> mp_from_mexpr expr
 
-let rec list_split_assoc k rev_before = function
+let is_modular = function
+  | SFBmodule _ | SFBmodtype _ -> true
+  | SFBconst _ | SFBmind _ -> false
+
+let rec list_split_assoc ((k,m) as km) rev_before = function
   | [] -> raise Not_found
-  | (k',b)::after when k=k' -> rev_before,b,after
-  | h::tail -> list_split_assoc k (h::rev_before) tail
+  | (k',b)::after when k=k' && is_modular b = m -> rev_before,b,after
+  | h::tail -> list_split_assoc km (h::rev_before) tail
 
 let discr_resolver env mtb =
      match mtb.typ_expr with
@@ -55,35 +59,34 @@ let rec rebuild_mp mp l =
 	
 let rec check_with env sign with_decl alg_sign mp equiv = 
   let sign,wd,equiv,cst= match with_decl with
-    | With_Definition (id,_) ->
-	let sign,cb,cst = check_with_aux_def env sign with_decl mp equiv in
-	  sign,With_definition_body(id,cb),equiv,cst
-    | With_Module (id,mp1) -> 
-	let sign,equiv,cst = 
-	  check_with_aux_mod env sign with_decl mp equiv in
-	  sign,With_module_body(id,mp1),equiv,cst in
+    | With_Definition (idl,c) ->
+	let sign,cb,cst = check_with_def env sign (idl,c) mp equiv in
+	sign,With_definition_body(idl,cb),equiv,cst
+    | With_Module (idl,mp1) ->
+	let sign,equiv,cst = check_with_mod env sign (idl,mp1) mp equiv in
+	sign,With_module_body(idl,mp1),equiv,cst
+  in
     if alg_sign = None then
       sign,None,equiv,cst
     else
       sign,Some (SEBwith(Option.get(alg_sign),wd)),equiv,cst
 	    
-and check_with_aux_def env sign with_decl mp equiv = 
+and check_with_def env sign (idl,c) mp equiv =
   let sig_b = match sign with 
     | SEBstruct(sig_b) -> sig_b
     | _ -> error_signature_expected sign
   in
-  let id,idl = match with_decl with
-    | With_Definition (id::idl,_) | With_Module (id::idl,_) -> id,idl
-    | With_Definition ([],_) | With_Module ([],_) -> assert false
+  let id,idl = match idl with
+    | [] -> assert false
+    | id::idl -> id,idl
   in
   let l = label_of_id id in
     try
-      let rev_before,spec,after = list_split_assoc l [] sig_b in
+      let rev_before,spec,after = list_split_assoc (l,(idl<>[])) [] sig_b in
       let before = List.rev rev_before in
       let env' = Modops.add_signature mp before equiv env in
-	match with_decl with
-          | With_Definition ([],_) -> assert false
-	  | With_Definition ([id],c) ->
+      if idl = [] then
+	      (* Toplevel definition *)
 	      let cb = match spec with
 		| SFBconst cb -> cb
 		| _ -> error_not_a_constant l
@@ -116,8 +119,9 @@ and check_with_aux_def env sign with_decl mp equiv =
 		    Cemitcodes.from_val (compile_constant_body env' def);
 		  const_constraints = cst }
 	      in
-	      SEBstruct(before@((l,SFBconst(cb'))::after)),cb',cst
-	  | With_Definition (_::_,c) ->
+	      SEBstruct(before@(l,SFBconst(cb'))::after),cb',cst
+      else
+	      (* Definition inside a sub-module *)
 	      let old = match spec with
 		| SFBmodule msb -> msb
 		| _ -> error_not_a_module (string_of_label l)
@@ -125,43 +129,36 @@ and check_with_aux_def env sign with_decl mp equiv =
 		begin
 		  match old.mod_expr with
                     | None ->
-			let new_with_decl = With_Definition (idl,c) in 
 			let sign,cb,cst = 
-			  check_with_aux_def env' old.mod_type new_with_decl 
+			  check_with_def env' old.mod_type (idl,c)
 			    (MPdot(mp,l)) old.mod_delta in
 			let new_spec = SFBmodule({old with
 						    mod_type = sign;
 						    mod_type_alg = None}) in
-			  SEBstruct(before@((l,new_spec)::after)),cb,cst
+			  SEBstruct(before@(l,new_spec)::after),cb,cst
                     | Some msb ->
 			error_generative_module_expected l
 		end
-	  | _ -> anomaly "Modtyping:incorrect use of with"
     with
       | Not_found -> error_no_such_label l
       | Reduction.NotConvertible -> error_incorrect_with_constraint l
 
-and check_with_aux_mod env sign with_decl mp equiv = 
+and check_with_mod env sign (idl,mp1) mp equiv = 
   let sig_b = match sign with 
     | SEBstruct(sig_b) ->sig_b
     | _ -> error_signature_expected sign
   in
-  let id,idl = match with_decl with
-    | With_Definition (id::idl,_) | With_Module (id::idl,_) -> id,idl
-    | With_Definition ([],_) | With_Module ([],_) -> assert false
+  let id,idl = match idl with
+    | [] -> assert false
+    | id::idl -> id,idl
   in
   let l = label_of_id id in
     try
-      let rev_before,spec,after = list_split_assoc l [] sig_b in
+      let rev_before,spec,after = list_split_assoc (l,true) [] sig_b in
       let before = List.rev rev_before in
-      let rec mp_rec = function
-	| [] -> mp
-	| i::r -> MPdot(mp_rec r,label_of_id i)
-      in
       let env' = Modops.add_signature mp before equiv env in
-	match with_decl with
-          | With_Module ([],_) -> assert false
-	  | With_Module ([id], mp1) ->
+      if idl = [] then
+	      (* Toplevel module definition *)
 	      let old = match spec with
 		  SFBmodule msb -> msb
 		| _ -> error_not_a_module (string_of_label l)
@@ -195,7 +192,8 @@ and check_with_aux_mod env sign with_decl mp equiv =
 	      let id_subst = map_mp (MPdot(mp,l)) (MPdot(mp,l)) new_mb.mod_delta in
 		SEBstruct(before@(l,new_spec)::subst_signature id_subst after),
 	      add_delta_resolver equiv new_mb.mod_delta,cst
-          | With_Module (idc,mp1) -> 
+      else
+	      (* Module definition of a sub-module *)
 	      let old = match spec with
 		  SFBmodule msb -> msb
 		| _ -> error_not_a_module (string_of_label l)
@@ -203,10 +201,9 @@ and check_with_aux_mod env sign with_decl mp equiv =
 	      begin
 		match old.mod_expr with
 		    None ->
-		      let new_with_decl = With_Module (idl,mp1) in
 		      let sign,equiv',cst =
-			check_with_aux_mod env'
-			  old.mod_type new_with_decl (MPdot(mp,l)) old.mod_delta in
+			check_with_mod env'
+			  old.mod_type (idl,mp1) (MPdot(mp,l)) old.mod_delta in
 		      let new_equiv = add_delta_resolver equiv equiv' in
 		      let new_spec = SFBmodule {old with 
 						  mod_type = sign;
@@ -224,7 +221,6 @@ and check_with_aux_mod env sign with_decl mp equiv =
 		  | _ ->
 		      error_generative_module_expected l
               end
-	  | _ -> anomaly "Modtyping:incorrect use of with"
     with
 	Not_found -> error_no_such_label l
       | Reduction.NotConvertible -> error_incorrect_with_constraint l
@@ -369,7 +365,7 @@ let rec add_struct_expr_constraints env = function
 
   | SEBstruct (structure_body) ->
       List.fold_left
-        (fun env (l,item) -> add_struct_elem_constraints env item)
+        (fun env (_,item) -> add_struct_elem_constraints env item)
         env
         structure_body
 
@@ -414,7 +410,7 @@ let rec struct_expr_constraints cst = function
 
   | SEBstruct (structure_body) ->
       List.fold_left
-        (fun cst (l,item) -> struct_elem_constraints cst item)
+        (fun cst (_,item) -> struct_elem_constraints cst item)
         cst
         structure_body
 
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index e87bc9c1c..94be2602e 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -102,7 +102,8 @@ type safe_environment =
     { old : safe_environment;
       env : env;
       modinfo : module_info;
-      labset : Labset.t;
+      modlabels : Labset.t;
+      objlabels : Labset.t;
       revstruct : structure_body;
       univ : Univ.constraints;
       engagement : engagement option;
@@ -110,13 +111,16 @@ 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 exists_modlabel l senv = Labset.mem l senv.modlabels
+let exists_objlabel l senv = Labset.mem l senv.objlabels
 
-let check_label l senv =
-  if exists_label l senv then error_existing_label l
+let check_modlabel l senv =
+  if exists_modlabel l senv then error_existing_label l
+let check_objlabel l senv =
+  if exists_objlabel l senv then error_existing_label l
 
-let check_labels ls senv =
-  Labset.iter (fun l -> check_label l senv) ls
+let check_objlabels ls senv =
+  Labset.iter (fun l -> check_objlabel l senv) ls
 
 let labels_of_mib mib =
   let add,get =
@@ -141,7 +145,8 @@ let rec empty_environment =
       variant = NONE;
       resolver = empty_delta_resolver;
       resolver_of_param = empty_delta_resolver};
-    labset = Labset.empty;
+    modlabels = Labset.empty;
+    objlabels = Labset.empty;
     revstruct = [];
     univ = Univ.empty_constraint;
     engagement = None;
@@ -173,11 +178,15 @@ type generic_name =
   | M
 
 let add_field ((l,sfb) as field) gn senv =
-  let labels = match sfb with
-    | SFBmind mib -> labels_of_mib mib
-    | _ -> Labset.singleton l
+  let mlabs,olabs = match sfb with
+    | SFBmind mib ->
+      let l = labels_of_mib mib in
+      check_objlabels l senv; (Labset.empty,l)
+    | SFBconst _ ->
+      check_objlabel l senv; (Labset.empty, Labset.singleton l)
+    | SFBmodule _ | SFBmodtype _ ->
+      check_modlabel l senv; (Labset.singleton l, Labset.empty)
   in
-  check_labels labels senv;
   let senv = add_constraints (constraints_of_sfb sfb) senv in
   let env' = match sfb, gn with
     | SFBconst cb, C con -> Environ.add_constant con cb senv.env
@@ -188,7 +197,8 @@ let add_field ((l,sfb) as field) gn senv =
   in
   { senv with
     env = env';
-    labset = Labset.union labels senv.labset;
+    modlabels = Labset.union mlabs senv.modlabels;
+    objlabels = Labset.union olabs senv.objlabels;
     revstruct = field :: senv.revstruct }
 
 (* Applying a certain function to the resolver of a safe environment *)
@@ -321,7 +331,7 @@ let add_module l me inl senv =
 (* Interactive modules *)
 
 let start_module l senv =
-  check_label l senv;
+  check_modlabel l senv;
  let mp = MPdot(senv.modinfo.modpath, l) in
  let modinfo = { modpath = mp;
 		 label = l;
@@ -332,7 +342,8 @@ let start_module l senv =
    mp, { old = senv;
 	 env = senv.env;
 	 modinfo = modinfo;
-	 labset = Labset.empty;
+	 modlabels = Labset.empty;
+	 objlabels = Labset.empty;
 	 revstruct = [];
          univ = Univ.empty_constraint;
          engagement = None;
@@ -416,7 +427,8 @@ let end_module l restype senv =
     mp,resolver,{ old = oldsenv.old;
 		  env = newenv;
 		  modinfo = modinfo;
-		  labset = Labset.add l oldsenv.labset;
+		  modlabels = Labset.add l oldsenv.modlabels;
+		  objlabels = oldsenv.objlabels;
 		  revstruct = (l,SFBmodule mb)::oldsenv.revstruct;
 		  univ = Univ.union_constraints senv'.univ oldsenv.univ;
 		  (* engagement is propagated to the upper level *)
@@ -511,7 +523,8 @@ let add_module_parameter mbid mte inl senv =
 				   variant = new_variant;
 				   resolver_of_param = add_delta_resolver
 			      resolver_of_param senv.modinfo.resolver_of_param};
-		     labset = senv.labset;
+		     modlabels = senv.modlabels;
+		     objlabels = senv.objlabels;
 		     revstruct = [];
 		     univ = senv.univ;
 		     engagement = senv.engagement;
@@ -523,7 +536,7 @@ let add_module_parameter mbid mte inl senv =
 (* Interactive module types *)
 
 let start_modtype l senv =
-  check_label l senv;
+  check_modlabel l senv;
  let mp = MPdot(senv.modinfo.modpath, l) in
  let modinfo = { modpath = mp;
 		 label = l;
@@ -534,7 +547,8 @@ let start_modtype l senv =
   mp, { old = senv;
 	env = senv.env;
 	modinfo = modinfo;
-	labset = Labset.empty;
+	modlabels = Labset.empty;
+	objlabels = Labset.empty;
 	revstruct = [];
         univ = Univ.empty_constraint;
         engagement = None;
@@ -585,7 +599,8 @@ let end_modtype l senv =
     mp, { old = oldsenv.old;
 	  env = newenv;
 	  modinfo = oldsenv.modinfo;
-	  labset = Labset.add l oldsenv.labset;
+	  modlabels = Labset.add l oldsenv.modlabels;
+	  objlabels = oldsenv.objlabels;
 	  revstruct = (l,SFBmodtype mtb)::oldsenv.revstruct;
           univ = Univ.union_constraints senv.univ oldsenv.univ;
           engagement = senv.engagement;
@@ -644,7 +659,8 @@ let start_library dir senv =
   mp, { old = senv;
 	env = senv.env;
 	modinfo = modinfo;
-	labset = Labset.empty;
+	modlabels = Labset.empty;
+	objlabels = Labset.empty;
 	revstruct = [];
         univ = Univ.empty_constraint;
         engagement = None;
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index 6f46a45be..ad275d49e 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -138,7 +138,7 @@ val typing : safe_environment -> constr -> judgment
 
 (** {7 Query } *)
 
-val exists_label : label -> safe_environment -> bool
+val exists_objlabel : label -> safe_environment -> bool
 
 (*spiwack: safe retroknowledge functionalities *)
 
diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml
index 9fb045407..46734b30b 100644
--- a/kernel/subtyping.ml
+++ b/kernel/subtyping.ml
@@ -33,15 +33,18 @@ type namedobject =
   | Constant of constant_body
   | IndType of inductive * mutual_inductive_body
   | IndConstr of constructor * mutual_inductive_body
+
+type namedmodule =
   | Module of module_body
   | Modtype of module_type_body
 
 (* adds above information about one mutual inductive: all types and
    constructors *)
 
-let add_nameobjects_of_mib ln mib map =
-  let add_nameobjects_of_one j oib map =
-    let ip = (ln,j) in
+let add_mib_nameobjects mp l mib map =
+  let ind = make_mind mp empty_dirpath l in
+  let add_mip_nameobjects j oib map =
+    let ip = (ind,j) in
     let map =
       array_fold_right_i
       (fun i id map ->
@@ -51,22 +54,33 @@ let add_nameobjects_of_mib ln mib map =
     in
       Labmap.add (label_of_id oib.mind_typename) (IndType (ip, mib)) map
   in
-    array_fold_right_i add_nameobjects_of_one mib.mind_packets map
+  array_fold_right_i add_mip_nameobjects mib.mind_packets map
+
+
+(* creates (namedobject/namedmodule) map for the whole signature *)
+
+type labmap = { objs : namedobject Labmap.t; mods : namedmodule Labmap.t }
 
+let empty_labmap = { objs = Labmap.empty; mods = Labmap.empty }
 
-(* creates namedobject map for the whole signature *)
+let get_obj mp map l =
+  try Labmap.find l map.objs
+  with Not_found -> error_no_such_label_sub l (string_of_mp mp)
 
-let make_label_map mp list =
+let get_mod mp map l =
+  try Labmap.find l map.mods
+  with Not_found -> error_no_such_label_sub l (string_of_mp mp)
+
+let make_labmap mp list =
   let add_one (l,e) map =
-   let add_map obj = Labmap.add l obj map in
    match e with
-    | SFBconst cb -> add_map (Constant cb)
-    | SFBmind mib ->
-       add_nameobjects_of_mib (make_mind mp empty_dirpath l) mib map
-    | SFBmodule mb -> add_map (Module mb)
-    | SFBmodtype mtb -> add_map (Modtype mtb)
+    | SFBconst cb -> { map with objs = Labmap.add l (Constant cb) map.objs }
+    | SFBmind mib -> { map with objs = add_mib_nameobjects mp l mib map.objs }
+    | SFBmodule mb -> { map with mods = Labmap.add l (Module mb) map.mods }
+    | SFBmodtype mtb -> { map with mods = Labmap.add l (Modtype mtb) map.mods }
   in
-    List.fold_right add_one list Labmap.empty
+  List.fold_right add_one list empty_labmap
+
 
 let check_conv_error error why cst f env a1 a2 =
   try
@@ -300,7 +314,6 @@ let check_constant cst env mp1 l info1 cb2 spec2 subst1 subst2 =
       let ty1 = type_of_constructor cstr (mind1,mind1.mind_packets.(i)) in
       let ty2 = Typeops.type_of_constant_type env cb2.const_type in
        check_conv NotConvertibleTypeField cst conv env ty1 ty2
-   | _ -> error DefinitionFieldExpected
 
 let rec check_modules cst env msb1 msb2 subst1 subst2 =
   let mty1 = module_type_of_module None msb1 in
@@ -309,33 +322,24 @@ let rec check_modules cst env msb1 msb2 subst1 subst2 =
     cst
 
 and check_signatures cst env mp1 sig1 mp2 sig2 subst1 subst2 reso1 reso2= 
-  let map1 = make_label_map mp1 sig1 in
+  let map1 = make_labmap mp1 sig1 in
   let check_one_body cst (l,spec2) =
-    let info1 =
-      try
-	Labmap.find l map1
-      with
-	  Not_found -> error_no_such_label_sub l
-	    (string_of_mp mp1)
-    in
-      match spec2 with
+    match spec2 with
 	| SFBconst cb2 ->
-	    check_constant cst env mp1 l info1 cb2 spec2 subst1 subst2
+	    check_constant cst env mp1 l (get_obj mp1 map1 l)
+	      cb2 spec2 subst1 subst2
 	| SFBmind mib2 ->
-	    check_inductive cst env
-	      mp1 l info1 mp2 mib2 spec2 subst1 subst2 reso1 reso2
+	    check_inductive cst env mp1 l (get_obj mp1 map1 l)
+	      mp2 mib2 spec2 subst1 subst2 reso1 reso2
 	| SFBmodule msb2 ->
-	    begin
-	      match info1 with
-		| Module msb -> check_modules cst env msb msb2 
-		    subst1 subst2
-		| _ -> error_signature_mismatch l spec2 ModuleFieldExpected
+	    begin match get_mod mp1 map1 l with
+	      | Module msb -> check_modules cst env msb msb2 subst1 subst2
+	      | _ -> error_signature_mismatch l spec2 ModuleFieldExpected
 	    end
 	| SFBmodtype mtb2 ->
-	    let mtb1 =
-	      match info1 with
-		| Modtype mtb -> mtb
-		| _ -> error_signature_mismatch l spec2 ModuleTypeFieldExpected
+	    let mtb1 = match get_mod mp1 map1 l with
+	      | Modtype mtb -> mtb
+	      | _ -> error_signature_mismatch l spec2 ModuleTypeFieldExpected
 	    in
 	    let env = add_module (module_body_of_type mtb2.typ_mp mtb2)
 	      (add_module (module_body_of_type mtb1.typ_mp mtb1) env) in
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
diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml
index 7c517dd9b..aa536b1dc 100644
--- a/plugins/extraction/extract_env.ml
+++ b/plugins/extraction/extract_env.ml
@@ -156,7 +156,9 @@ let factor_fix env l cb msb =
 	 function
 	   | (l,SFBconst cb') ->
 	       let check' = check_fix env cb' (j+1) in
-	       if not (fst check = fst check' && prec_declaration_equal (snd check) (snd check')) then raise Impossible;
+	       if not (fst check = fst check' &&
+		   prec_declaration_equal (snd check) (snd check'))
+	       then raise Impossible;
 	       labels.(j+1) <- l;
 	   | _ -> raise Impossible) msb';
     labels, recd, msb''
@@ -197,13 +199,14 @@ let rec msid_of_seb = function
   | SEBwith (seb,_) -> msid_of_seb seb
   | _ -> assert false
 
-let env_for_mtb_with env mp seb idl =
+let env_for_mtb_with_def env mp seb idl =
   let sig_b = match seb with
     | SEBstruct(sig_b) -> sig_b
     | _ -> assert false
   in
   let l = label_of_id (List.hd idl) in
-  let before = fst (list_split_when (fun (l',_) -> l=l') sig_b) in
+  let spot = function (l',SFBconst _) -> l = l' | _ -> false in
+  let before = fst (list_split_when spot sig_b) in
   Modops.add_signature mp before empty_delta_resolver env
 
 (* From a [structure_body] (i.e. a list of [structure_field_body])
@@ -242,7 +245,7 @@ let rec extract_sfb_spec env mp = function
 and extract_seb_spec env mp1 (seb,seb_alg) = match seb_alg with
   | SEBident mp -> Visit.add_mp_all mp; MTident mp
   | SEBwith(seb',With_definition_body(idl,cb))->
-      let env' = env_for_mtb_with env (msid_of_seb seb') seb idl in
+      let env' = env_for_mtb_with_def env (msid_of_seb seb') seb idl in
       let mt = extract_seb_spec env mp1 (seb,seb') in
       (match extract_with_type env' cb with (* cb peut contenir des kn  *)
 	 | None -> mt
diff --git a/plugins/extraction/modutil.ml b/plugins/extraction/modutil.ml
index 123edd4c3..6380ee7ec 100644
--- a/plugins/extraction/modutil.ml
+++ b/plugins/extraction/modutil.ml
@@ -195,6 +195,15 @@ let signature_of_structure s =
 
 (*s Searching one [ml_decl] in a [ml_structure] by its [global_reference] *)
 
+let is_modular = function
+  | SEdecl _ -> false
+  | SEmodule _ | SEmodtype _ -> true
+
+let rec search_structure l m = function
+  | [] -> raise Not_found
+  | (lab,d)::_ when lab=l && is_modular d = m -> d
+  | _::fields -> search_structure l m fields
+
 let get_decl_in_structure r struc =
   try
     let base_mp,ll = labels_of_ref r in
@@ -203,7 +212,7 @@ let get_decl_in_structure r struc =
     let rec go ll sel = match ll with
       | [] -> assert false
       | l :: ll ->
-	  match List.assoc l sel with
+	  match search_structure l (ll<>[]) sel with
 	    | SEdecl d -> d
 	    | SEmodtype m -> assert false
 	    | SEmodule m ->