diff options
Diffstat (limited to 'library/summary.mli')
| -rw-r--r-- | library/summary.mli | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/library/summary.mli b/library/summary.mli index 7f300a996..3e6375b0e 100644 --- a/library/summary.mli +++ b/library/summary.mli @@ -28,5 +28,9 @@ val section_unfreeze_summaries : frozen -> unit val module_unfreeze_summaries : frozen -> unit val init_summaries : unit -> unit - +(** Beware: if some code is dynamically loaded via dynlink after the + initialization of Coq, the init functions of any summary declared + by this code may not be run. It is hence the responsability of + plugins to initialize themselves properly. +*) |