diff options
| author | Théo Zimmermann | 2020-06-04 18:38:02 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2020-06-04 19:27:20 +0200 |
| commit | 08e73f23b7fd26bf84f9b36156f9ac9cab51ac4d (patch) | |
| tree | 144ec4ffee609101c1ca0bd1884127fa9e4bf2ef /doc/sphinx/proof-engine | |
| parent | db768e6828af62e06eb03d36509be6f8fc1efbf3 (diff) | |
Document known issue of Proof <term> with PG.
See #12444.
Diffstat (limited to 'doc/sphinx/proof-engine')
| -rw-r--r-- | doc/sphinx/proof-engine/proof-handling.rst | 9 |
1 files changed, 9 insertions, 0 deletions
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 + <https://github.com/ProofGeneral/PG/issues/498>`_). + .. cmd:: Proof Is a no-op which is useful to delimit the sequence of tactic commands |