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 9d2f2c2d9..aed7274d0 100644
--- a/stm/stm.mli
+++ b/stm/stm.mli
@@ -284,3 +284,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