diff options
Diffstat (limited to 'stm/stm.mli')
| -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 f1bef2dc4d..92a782d965 100644 --- a/stm/stm.mli +++ b/stm/stm.mli @@ -119,6 +119,8 @@ the specified state AND that has differences in the underlying proof (i.e., ignoring proofview-only changes). Used to compute proof diffs. *) val get_prev_proof : doc:doc -> Stateid.t -> Proof.t option +val get_proof : doc:doc -> Stateid.t -> Proof.t option + (* [query at ?report_with cmd] Executes [cmd] at a given state [at], throwing away side effects except messages. Feedback will be sent with [report_with], which defaults to the dummy state id *) |