From a4d48ce98d7ae0cf07c653ed75700ed6f182936a Mon Sep 17 00:00:00 2001
From: Pierre Letouzey
Date: Mon, 30 Nov 2015 16:40:46 +0100
Subject: Extraction: check for remaining implicits after dead code removal
 (fix #4243)

---
 plugins/extraction/modutil.ml | 22 +++++++++++++---------
 1 file changed, 13 insertions(+), 9 deletions(-)

(limited to 'plugins')

diff --git a/plugins/extraction/modutil.ml b/plugins/extraction/modutil.ml
index 8158ac647e..53c9f59878 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
-- 
cgit v1.2.3