From 18c3b336781e2c248a44ff9209cb8bf7eb5f38a3 Mon Sep 17 00:00:00 2001 From: gareuselesinge Date: Fri, 30 Aug 2013 16:02:23 +0000 Subject: summary for ML modules made correct This summary entry is special because its unfreeze may load ML code that in turns adds summary entries. Hence it is the first summary piece to be unfreezed, otherwise some summaries may get lost. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16752 85f007b7-540e-0410-9357-904b9bb8a0f7 --- library/summary.ml | 15 +++++++++++++-- 1 file changed, 13 insertions(+), 2 deletions(-) (limited to 'library/summary.ml') diff --git a/library/summary.ml b/library/summary.ml index b46ce85b1..d1bbf7191 100644 --- a/library/summary.ml +++ b/library/summary.ml @@ -59,11 +59,22 @@ let freeze_summaries ~marshallable = summaries; !m +let ml_modules = "ML-MODULES" +let ml_modules_summary = mangle ml_modules + let unfreeze_summaries fs = + (* The unfreezing of [ml_modules_summary] has to be anticipated since it + * may modify the content of [summaries] ny loading new ML modules *) + (try + (Hashtbl.find summaries ml_modules_summary).unfreeze_function + (String.Map.find ml_modules_summary fs) + with Not_found -> anomaly (str"Undeclared summary "++str ml_modules_summary)); Hashtbl.iter (fun id decl -> - try decl.unfreeze_function (String.Map.find id fs) - with Not_found -> decl.init_function()) + if id = ml_modules_summary then () (* already unfreezed *) + else + try decl.unfreeze_function (String.Map.find id fs) + with Not_found -> decl.init_function()) summaries let init_summaries () = -- cgit v1.2.3