diff options
| author | Jim Fehrle | 2019-06-08 05:04:41 -0700 |
|---|---|---|
| committer | Jim Fehrle | 2019-06-25 12:45:03 -0700 |
| commit | 403917b7d9ecb2ddfaaac2185c355d415d5fa5bc (patch) | |
| tree | e5afcff136068558ac11b7643709be9a7710ebd5 /doc | |
| parent | 7dfcb0f7c817e66280ab37b6c653b5596a16c249 (diff) | |
Re-add the "Show Goal" command for Prooftree in PG.
It prints a goal given its internal goal id and the Stm state id.
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 |