diff options
| author | Théo Zimmermann | 2020-05-08 12:34:14 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2020-05-08 12:34:14 +0200 |
| commit | a95ff1f5d8651a787c59acc1b5040a589725eb3b (patch) | |
| tree | 2483c3fe766f7936a31129bb8194ffa6b59ec8d9 | |
| parent | ca04e600e035b6822d1178cafd33848ca27446d4 (diff) | |
| parent | 665ace812f4770e8ac713d8f9c5583553c2055a8 (diff) | |
Merge PR #12281: [doc] named lemmas can be Saved too
Reviewed-by: Zimmi48
| -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 ------------------------------------------------ |