diff options
| author | Théo Zimmermann | 2020-06-04 21:36:00 +0200 |
|---|---|---|
| committer | GitHub | 2020-06-04 21:36:00 +0200 |
| commit | f47b2edfb9e43d551c3b243c16cfc10e38e70d47 (patch) | |
| tree | f766d00d8e7fe1737d39f37d8d525a2f3ef56dd1 /doc/sphinx/proof-engine | |
| parent | 08e73f23b7fd26bf84f9b36156f9ac9cab51ac4d (diff) | |
Tweak wording.
Co-authored-by: Jim Fehrle <jim.fehrle@gmail.com>
Diffstat (limited to 'doc/sphinx/proof-engine')
| -rw-r--r-- | doc/sphinx/proof-engine/proof-handling.rst | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/doc/sphinx/proof-engine/proof-handling.rst b/doc/sphinx/proof-engine/proof-handling.rst index 1933d52c1a..df5e4737b9 100644 --- a/doc/sphinx/proof-engine/proof-handling.rst +++ b/doc/sphinx/proof-engine/proof-handling.rst @@ -127,10 +127,10 @@ list of assertion commands is given in :ref:`Assertions`. The command .. warning:: - The use of this command is discouraged. In particular, it is - known to not work in Proof General because this command must - immediately follow the command that opened the proof mode, but - Proof General inserts :cmd:`Unset` :flag:`Silent` before (see + Use of this command is discouraged. In particular, it + doesn't work in Proof General because it must + immediately follow the command that opened proof mode, but + Proof General inserts :cmd:`Unset` :flag:`Silent` before it (see `Proof General issue #498 <https://github.com/ProofGeneral/PG/issues/498>`_). |