diff options
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/changelog/07-commands-and-options/10277-no-show-script.rst | 2 | ||||
| -rw-r--r-- | doc/changelog/12-misc/10019-PG-proof-diffs.rst | 3 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/proof-handling.rst | 20 |
3 files changed, 9 insertions, 16 deletions
diff --git a/doc/changelog/07-commands-and-options/10277-no-show-script.rst b/doc/changelog/07-commands-and-options/10277-no-show-script.rst new file mode 100644 index 0000000000..7fdeb632b4 --- /dev/null +++ b/doc/changelog/07-commands-and-options/10277-no-show-script.rst @@ -0,0 +1,2 @@ +- Remove ``Show Script`` command (deprecated since 8.10) + (`#10277 <https://github.com/coq/coq/pull/10277>`_, by Gaëtan Gilbert). diff --git a/doc/changelog/12-misc/10019-PG-proof-diffs.rst b/doc/changelog/12-misc/10019-PG-proof-diffs.rst new file mode 100644 index 0000000000..b2d191be26 --- /dev/null +++ b/doc/changelog/12-misc/10019-PG-proof-diffs.rst @@ -0,0 +1,3 @@ +- Proof General can now display Coq-generated diffs between proof steps + in color. (`#10019 <https://github.com/coq/coq/pull/10019>`_ and (in Proof General) + `#421 <https://github.com/ProofGeneral/PG/pull/421>`_, by Jim Fehrle). diff --git a/doc/sphinx/proof-engine/proof-handling.rst b/doc/sphinx/proof-engine/proof-handling.rst index 3f966755ca..0cff987a27 100644 --- a/doc/sphinx/proof-engine/proof-handling.rst +++ b/doc/sphinx/proof-engine/proof-handling.rst @@ -535,19 +535,6 @@ Requesting information eexists ?[n]. Show n. - .. cmdv:: Show Script - :name: Show Script - - Displays the whole list of tactics applied from the - beginning of the current proof. This tactics script may contain some - holes (subgoals not yet proved). They are printed under the form - - ``<Your Tactic Text here>``. - - .. deprecated:: 8.10 - - Please use a text editor. - .. cmdv:: Show Proof :name: Show Proof @@ -705,9 +692,10 @@ command in CoqIDE. You can change the background colors shown for diffs from th lets you control other attributes of the highlights, such as the foreground color, bold, italic, underline and strikeout. -Note: As of this writing (August 2018), Proof General will need minor changes -to be able to show diffs correctly. We hope it will support this feature soon. -See https://github.com/ProofGeneral/PG/issues/381 for the current status. +As of June 2019, Proof General can also display Coq-generated proof diffs automatically. +Please see the PG documentation section +"`Showing Proof Diffs" <https://proofgeneral.github.io/doc/master/userman/Coq-Proof-General#Showing-Proof-Diffs>`_) +for details. How diffs are calculated ```````````````````````` |