diff options
| -rw-r--r-- | stm/stm.mli | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/stm/stm.mli b/stm/stm.mli index fd306425c1..e5327cb838 100644 --- a/stm/stm.mli +++ b/stm/stm.mli @@ -38,6 +38,8 @@ val edit_at : Stateid.t -> [ `NewTip | `Focus of focus ] (* Evaluates the tip of the current branch *) val finish : unit -> unit +val observe : Stateid.t -> unit + val stop_worker : int -> unit (* Joins the entire document. Implies finish, but also checks proofs *) |