From 665ace812f4770e8ac713d8f9c5583553c2055a8 Mon Sep 17 00:00:00 2001
From: Antonio Nikishaev
Date: Fri, 8 May 2020 12:25:08 +0400
Subject: doc: one can save named lemmas Save too

---
 doc/sphinx/proof-engine/proof-handling.rst | 6 ++----
 1 file changed, 2 insertions(+), 4 deletions(-)

(limited to 'doc/sphinx/proof-engine')

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
 ------------------------------------------------
-- 
cgit v1.2.3