aboutsummaryrefslogtreecommitdiffhomepage
path: root/library/summary.ml
diff options
context:
space:
mode:
authorGravatar Enrico Tassi <enrico.tassi@inria.fr>2015-03-25 16:57:55 +0100
committerGravatar Enrico Tassi <enrico.tassi@inria.fr>2015-03-25 16:57:55 +0100
commit7c7ceb48c12cad0bcfd59e1e8ae944d7c6137cbe (patch)
treeb546d7903d3d10222d7a3bba902e96119c544372 /library/summary.ml
parent99ed6c907c3b2c4901ba51446e0b67696929e02e (diff)
Summary: fix code to detect functional values in summary
Diffstat (limited to 'library/summary.ml')
-rw-r--r--library/summary.ml1
1 files changed, 1 insertions, 0 deletions
diff --git a/library/summary.ml b/library/summary.ml
index 7e7628a1b..8e2abbf15 100644
--- a/library/summary.ml
+++ b/library/summary.ml
@@ -66,6 +66,7 @@ let freeze_summaries ~marshallable : frozen =
let fold id (_, decl) accu =
(* to debug missing Lazy.force
if marshallable <> `No then begin
+ let id, _ = Int.Map.find id !summaries in
prerr_endline ("begin marshalling " ^ id);
ignore(Marshal.to_string (decl.freeze_function marshallable) []);
prerr_endline ("end marshalling " ^ id);