From 403917b7d9ecb2ddfaaac2185c355d415d5fa5bc Mon Sep 17 00:00:00 2001
From: Jim Fehrle
Date: Sat, 8 Jun 2019 05:04:41 -0700
Subject: Re-add the "Show Goal" command for Prooftree in PG. It prints a goal
 given its internal goal id and the Stm state id.

---
 stm/stm.ml | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'stm/stm.ml')

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 =
-- 
cgit v1.2.3