Merge PR #10356: Re-add the "Show Goal" command for Prooftree in PG.

Reviewed-by: Zimmi48
Reviewed-by: ejgallego
Reviewed-by: gares
Ack-by: herbelin
Ack-by: jfehrle

2 files changed, 4 insertions, 0 deletions

diff --git a/stm/stm.ml b/stm/stm.ml
index 91397950f6..e04277b052 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -1114,6 +1114,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 (* {{{ *)
 
@@ -1259,6 +1260,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 *)