diff options
| author | Maxime Dénès | 2017-10-09 16:44:02 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-10-09 16:44:02 +0200 |
| commit | 1aeb43a3c7779001b0404d9dcc1603bf4c49dee0 (patch) | |
| tree | eea4ffe8d6a2e60ae134efab678e5a878a303097 /API/API.mli | |
| parent | 5ef85c86dc94338c2d0da060946baafea2e5370e (diff) | |
| parent | 75c0c5c2b460614fba6705c6e0d64859815a613c (diff) | |
Merge PR #1087: [stm] Switch to a functional API
Diffstat (limited to 'API/API.mli')
| -rw-r--r-- | API/API.mli | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/API/API.mli b/API/API.mli index 3bd047043a..254cc2215b 100644 --- a/API/API.mli +++ b/API/API.mli @@ -5813,8 +5813,11 @@ end module Stm : sig + type doc type state - val state_of_id : + + val get_doc : Feedback.doc_id -> doc + val state_of_id : doc:doc -> Stateid.t -> [ `Valid of state option | `Expired | `Error of exn ] end |