diff options
Diffstat (limited to 'doc/sphinx/proof-engine')
| -rw-r--r-- | doc/sphinx/proof-engine/proof-handling.rst | 6 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/ssreflect-proof-language.rst | 2 |
2 files changed, 3 insertions, 5 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 ------------------------------------------------ diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst index 28c5359a04..4be18ccda9 100644 --- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst +++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst @@ -286,7 +286,7 @@ example, the null and all list function(al)s can be defined as follows: .. coqtop:: all Variable d: Set. - Fixpoint null (s : list d) := + Definition null (s : list d) := if s is nil then true else false. Variable a : d -> bool. Fixpoint all (s : list d) : bool := |