From 61dc740ed1c3780cccaec00d059a28f0d31d0052 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Mon, 4 Jun 2012 12:07:52 +0200 Subject: Imported Upstream version 8.4~gamma0+really8.4beta2 --- plugins/extraction/modutil.ml | 11 ++++++++++- 1 file changed, 10 insertions(+), 1 deletion(-) (limited to 'plugins/extraction/modutil.ml') 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 -> -- cgit v1.2.3