diff options
| author | Antonio Nikishaev | 2020-05-08 12:25:08 +0400 |
|---|---|---|
| committer | Antonio Nikishaev | 2020-05-08 12:52:05 +0400 |
| commit | 665ace812f4770e8ac713d8f9c5583553c2055a8 (patch) | |
| tree | 4626b43a9bf6a58732cbf9e617b8b8ffb3e25750 /doc/sphinx/proof-engine | |
| parent | e4bfbdfc4b4944d6e6d702eb732bce24f962e67f (diff) | |
doc: one can save named lemmas Save too
Diffstat (limited to 'doc/sphinx/proof-engine')
| -rw-r--r-- | doc/sphinx/proof-engine/proof-handling.rst | 6 |
1 files changed, 2 insertions, 4 deletions
diff --git a/doc/sphinx/proof-engine/proof-handling.rst b/doc/sphinx/proof-engine/proof-handling.rst index 3b5233502d..cf4d432f64 100644 --- a/doc/sphinx/proof-engine/proof-handling.rst +++ b/doc/sphinx/proof-engine/proof-handling.rst @@ -90,9 +90,7 @@ list of assertion commands is given in :ref:`Assertions`. The command .. cmd:: Save @ident :name: Save - Forces the name of the original goal to be :token:`ident`. This - command can only be used if the original goal - was opened using the :cmd:`Goal` command. + Forces the name of the original goal to be :token:`ident`. .. cmd:: Admitted @@ -821,7 +819,7 @@ in compacted hypotheses: .. .. image:: ../_static/diffs-coqide-compacted.png - :alt: coqide with Set Diffs on with compacted hyptotheses + :alt: coqide with Set Diffs on with compacted hypotheses Controlling the effect of proof editing commands ------------------------------------------------ |