diff options
| author | Jim Fehrle | 2018-08-08 18:45:47 -0700 |
|---|---|---|
| committer | Jim Fehrle | 2018-09-17 10:33:27 -0700 |
| commit | a828bcedb8ad60c5b1f4cf71f92f24f2c1197ecb (patch) | |
| tree | 372fd5a8c6f880db4f246ea5b6f498a7393bc737 /stm/stm.mli | |
| parent | f1482433ff225831d9937753f946cff2577b9309 (diff) | |
Ensure_prev_proof returns a proof that has underlying differences from
the specified version (i.e., skip over versions with proofview-only differences).
Diffstat (limited to 'stm/stm.mli')
| -rw-r--r-- | stm/stm.mli | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/stm/stm.mli b/stm/stm.mli index 7f70ea18da..1e5ceb7e23 100644 --- a/stm/stm.mli +++ b/stm/stm.mli @@ -111,7 +111,8 @@ val add : doc:doc -> ontop:Stateid.t -> ?newtip:Stateid.t -> doc * Stateid.t * [ `NewTip | `Unfocus of Stateid.t ] (* Returns the proof state before the last tactic that was applied at or before -the specified state. Used to compute proof diffs. *) +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 (* [query at ?report_with cmd] Executes [cmd] at a given state [at], |