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.mli | 5 +++++ 1 file changed, 5 insertions(+) (limited to 'library/summary.mli') 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. *) -- cgit v1.2.3