blob: 3e6375b0e8c64d12769942db983b14f85bcb35c4 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
(*i $Id$ i*)
(* This module registers the declaration of global tables, which will be kept
in synchronization during the various backtracks of the system. *)
type 'a summary_declaration = {
freeze_function : unit -> 'a;
unfreeze_function : 'a -> unit;
init_function : unit -> unit;
survive_module : bool; (* should be false is most cases *)
survive_section : bool }
val declare_summary : string -> 'a summary_declaration -> unit
type frozen
val freeze_summaries : unit -> frozen
val unfreeze_summaries : frozen -> unit
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.
*)
|
