diff options
| author | Jim Fehrle | 2019-06-08 05:04:41 -0700 |
|---|---|---|
| committer | Jim Fehrle | 2019-06-25 12:45:03 -0700 |
| commit | 403917b7d9ecb2ddfaaac2185c355d415d5fa5bc (patch) | |
| tree | e5afcff136068558ac11b7643709be9a7710ebd5 /stm | |
| parent | 7dfcb0f7c817e66280ab37b6c653b5596a16c249 (diff) | |
Re-add the "Show Goal" command for Prooftree in PG.
It prints a goal given its internal goal id and the Stm state id.
Diffstat (limited to 'stm')
| -rw-r--r-- | stm/stm.ml | 2 | ||||
| -rw-r--r-- | stm/stm.mli | 2 |
2 files changed, 4 insertions, 0 deletions
diff --git a/stm/stm.ml b/stm/stm.ml index 28d5447c44..0216eef75f 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -1105,6 +1105,7 @@ module Backtrack : sig (* Returns the state that the command should backtract to *) val undo_vernac_classifier : vernac_control -> doc:doc -> Stateid.t val get_prev_proof : doc:doc -> Stateid.t -> Proof.t option + val get_proof : doc:doc -> Stateid.t -> Proof.t option end = struct (* {{{ *) @@ -1250,6 +1251,7 @@ end = struct (* {{{ *) end (* }}} *) let get_prev_proof = Backtrack.get_prev_proof +let get_proof = Backtrack.get_proof let hints = ref Aux_file.empty_aux_file let set_compilation_hints file = 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 *) |