diff options
Diffstat (limited to 'plugins/extraction/modutil.ml')
| -rw-r--r-- | plugins/extraction/modutil.ml | 11 |
1 files changed, 10 insertions, 1 deletions
diff --git a/plugins/extraction/modutil.ml b/plugins/extraction/modutil.ml index 9e8dd828..4e0dbcab 100644 --- a/plugins/extraction/modutil.ml +++ b/plugins/extraction/modutil.ml @@ -194,6 +194,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 @@ -202,7 +211,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 -> |