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.

---
 doc/sphinx/proof-engine/proof-handling.rst | 8 ++++++++
 1 file changed, 8 insertions(+)

(limited to 'doc')

diff --git a/doc/sphinx/proof-engine/proof-handling.rst b/doc/sphinx/proof-engine/proof-handling.rst
index 0cff987a27..03b30d5d97 100644
--- a/doc/sphinx/proof-engine/proof-handling.rst
+++ b/doc/sphinx/proof-engine/proof-handling.rst
@@ -600,6 +600,14 @@ Requesting information
       its normalized form at the current stage of the proof, useful for
       debugging universe inconsistencies.
 
+   .. cmdv:: Show Goal @num at @num
+      :name: Show Goal
+
+      This command is only available in coqtop.  Displays a goal at a
+      proof state using the goal ID number and the proof state ID number.
+      It is primarily for use by tools such as Prooftree that need to fetch
+      goal history in this way.  Prooftree is a tool for visualizing a proof
+      as a tree that runs in Proof General.
 
 .. cmd:: Guarded
 
-- 
cgit v1.2.3