aboutsummaryrefslogtreecommitdiffhomepage
path: root/stm/stm.mli
diff options
context:
space:
mode:
Diffstat (limited to 'stm/stm.mli')
-rw-r--r--stm/stm.mli4
1 files changed, 4 insertions, 0 deletions
diff --git a/stm/stm.mli b/stm/stm.mli
index 7a720aa72..35ce77a38 100644
--- a/stm/stm.mli
+++ b/stm/stm.mli
@@ -283,3 +283,7 @@ val get_all_proof_names : doc:doc -> Id.t list
(** Enable STM debugging *)
val stm_debug : bool ref
+
+type document
+val backup : unit -> document
+val restore : document -> unit