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

1 files changed, 10 insertions, 1 deletions

diff --git a/plugins/extraction/modutil.ml b/plugins/extraction/modutil.ml
index 123edd4c3f..6380ee7ecb 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 ->