diff options
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/sphinx/proof-engine/proof-handling.rst | 8 |
1 files changed, 8 insertions, 0 deletions
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 |