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.mli | |
| 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.mli')
| -rw-r--r-- | library/summary.mli | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/library/summary.mli b/library/summary.mli index 38d5fc7e8..f6a9c6951 100644 --- a/library/summary.mli +++ b/library/summary.mli @@ -42,6 +42,11 @@ val declare_summary : string -> 'a summary_declaration -> unit val ref : ?freeze:(marshallable -> 'a -> 'a) -> name:string -> 'a -> 'a ref +(** Special name for the summary of ML modules. This summary entry is + special because its unfreeze may load ML code and hence add summary + entries. Thus is has to be recognizable, and handled appropriately *) +val ml_modules : string + (** For global tables registered statically before the end of coqtop launch, the following empty [init_function] could be used. *) |