blob: 5db9617be0b1dc4bcc29b898a22359a47a67645e (
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
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
(*i $Id: summary.mli 14641 2011-11-06 11:59:10Z herbelin $ 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 }
val declare_summary : string -> 'a summary_declaration -> unit
type frozen
val freeze_summaries : unit -> frozen
val 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.
*)
|
