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

2 files changed, 17 insertions, 5 deletions

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