diff options
| author | Hugo Herbelin | 2020-10-04 21:51:00 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2020-10-06 21:59:07 +0200 |
| commit | 3b8252d8990e715e5954812dffd0a5986cbb6012 (patch) | |
| tree | 8993a75d8ad87b0bf9cad9de02ddfc5a75f91042 /doc/sphinx/proof-engine | |
| parent | bd57c1a48cca55be374e597e2d89fe619a39c26e (diff) | |
Documenting option Set Printing Goal Name.
Diffstat (limited to 'doc/sphinx/proof-engine')
| -rw-r--r-- | doc/sphinx/proof-engine/proof-handling.rst | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/doc/sphinx/proof-engine/proof-handling.rst b/doc/sphinx/proof-engine/proof-handling.rst index f90ebadb3a..6c94baf959 100644 --- a/doc/sphinx/proof-engine/proof-handling.rst +++ b/doc/sphinx/proof-engine/proof-handling.rst @@ -858,6 +858,11 @@ Controlling the effect of proof editing commands proved before starting the previous proof) and Coq will switch back to the proof of the previous assertion. +.. flag:: Printing Goal Names + + When turned on, the name of the goal is printed in interactive + proof mode, which can be useful in cases of cross references + between goals. Controlling memory usage ------------------------ |