diff options
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. *) |