From 08e73f23b7fd26bf84f9b36156f9ac9cab51ac4d Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Thu, 4 Jun 2020 18:38:02 +0200 Subject: Document known issue of Proof with PG. See #12444. --- doc/sphinx/proof-engine/proof-handling.rst | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/doc/sphinx/proof-engine/proof-handling.rst b/doc/sphinx/proof-engine/proof-handling.rst index cf4d432f64..1933d52c1a 100644 --- a/doc/sphinx/proof-engine/proof-handling.rst +++ b/doc/sphinx/proof-engine/proof-handling.rst @@ -125,6 +125,15 @@ list of assertion commands is given in :ref:`Assertions`. The command That is, you have to give the full proof in one gulp, as a proof term (see Section :ref:`applyingtheorems`). + .. 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 + `Proof General issue #498 + `_). + .. cmd:: Proof Is a no-op which is useful to delimit the sequence of tactic commands -- cgit v1.2.3 From f47b2edfb9e43d551c3b243c16cfc10e38e70d47 Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Thu, 4 Jun 2020 21:36:00 +0200 Subject: Tweak wording. Co-authored-by: Jim Fehrle --- doc/sphinx/proof-engine/proof-handling.rst | 8 ++++---- 1 file 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 `_). -- cgit v1.2.3