aboutsummaryrefslogtreecommitdiffhomepage
path: root/stm/stm.mli
diff options
context:
space:
mode:
Diffstat (limited to 'stm/stm.mli')
-rw-r--r--stm/stm.mli2
1 files changed, 1 insertions, 1 deletions
diff --git a/stm/stm.mli b/stm/stm.mli
index 6ffe0beb4..d825ff33e 100644
--- a/stm/stm.mli
+++ b/stm/stm.mli
@@ -122,7 +122,7 @@ type state = {
proof : Proof_global.state;
shallow : bool
}
-val state_of_id : Stateid.t -> [ `Valid of state option | `Expired ]
+val state_of_id : Stateid.t -> [ `Valid of state option | `Expired | `Error of exn ]
(** read-eval-print loop compatible interface ****************************** **)