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.mli | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'stm/stm.mli')

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