diff options
| author |  Pierre Letouzey <pierre.letouzey@inria.fr> | 2015-11-30 16:40:46 +0100 |
|---|---|---|
| committer | Pierre Letouzey <pierre.letouzey@inria.fr> | 2015-12-12 18:51:37 +0100 |
| commit | a4d48ce98d7ae0cf07c653ed75700ed6f182936a (patch) | |
| tree | a31e0fd5c30146d6feba0a287b2ebe09d56ac6dd | |
| parent | e2915d2e615a271c90d9e8c8599a428ed15828b5 (diff) | |
Extraction: check for remaining implicits after dead code removal (fix #4243)
| -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 |