diff options
| author | Emilio Jesus Gallego Arias | 2020-06-05 17:39:42 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-06-05 17:39:42 +0200 |
| commit | e9bba6f73ef3d66949f2527cbd250d1c45210add (patch) | |
| tree | 34bc900bc215388dd1397d03c42d72de3212c5c8 | |
| parent | 2f2d21a6102f8cbbdb3d23624c15d05a6e52345c (diff) | |
| parent | f47b2edfb9e43d551c3b243c16cfc10e38e70d47 (diff) | |
Merge PR #12450: Document known issue of Proof <term> with PG.
Reviewed-by: ejgallego
Reviewed-by: erikmd
Reviewed-by: jfehrle
| -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..df5e4737b9 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:: + + 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>`_). + .. cmd:: Proof Is a no-op which is useful to delimit the sequence of tactic commands |