diff options
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/extraction/modutil.ml | 22 |
1 files changed, 13 insertions, 9 deletions
diff --git a/plugins/extraction/modutil.ml b/plugins/extraction/modutil.ml index 8158ac647..53c9f5987 100644 --- a/plugins/extraction/modutil.ml +++ b/plugins/extraction/modutil.ml @@ -404,12 +404,16 @@ let optimize_struct to_appear struc = List.map (fun (mp,lse) -> (mp, optim_se true (fst to_appear) subst lse)) struc in - ignore (struct_ast_search check_implicits opt_struc); - if library () then - List.filter (fun (_,lse) -> not (List.is_empty lse)) opt_struc - else begin - reset_needed (); - List.iter add_needed (fst to_appear); - List.iter add_needed_mp (snd to_appear); - depcheck_struct opt_struc - end + let mini_struc = + if library () then + List.filter (fun (_,lse) -> not (List.is_empty lse)) opt_struc + else + begin + reset_needed (); + List.iter add_needed (fst to_appear); + List.iter add_needed_mp (snd to_appear); + depcheck_struct opt_struc + end + in + ignore (struct_ast_search check_implicits mini_struc); + mini_struc |