diff options
| author |  gareuselesinge <gareuselesinge@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-08-30 16:02:23 +0000 |
|---|---|---|
| committer | gareuselesinge <gareuselesinge@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-08-30 16:02:23 +0000 |
| commit | 18c3b336781e2c248a44ff9209cb8bf7eb5f38a3 (patch) | |
| tree | 55ed6563117e4d3ca43d70e922db48ac28e8c3ae /library/summary.ml | |
| parent | 81117e3da0d2a75610c861e466088c311b3727d0 (diff) | |
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
Diffstat (limited to 'library/summary.ml')
| -rw-r--r-- | library/summary.ml | 15 |
1 files changed, 13 insertions, 2 deletions
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 () = |