diff options
| author | Théo Zimmermann | 2019-06-03 16:27:19 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2019-06-03 16:27:19 +0200 |
| commit | 5465bbf5525ce82fd3063f6cbd0bb651cc5f4d24 (patch) | |
| tree | f168714642f5a819e7b0e08941609fed988761a7 | |
| parent | 7032085c809993d6a173e51aec447c02828ae070 (diff) | |
| parent | b2f70d5c203a68af4c7048b417eb0dc82cee2610 (diff) | |
Merge PR #10261: Update doc to reflect that PG now supports Coq-generated proof diffs
Reviewed-by: Zimmi48
Reviewed-by: cpitclaudel
Ack-by: erikmd
| -rw-r--r-- | doc/changelog/12-misc/10019-PG-proof-diffs.rst | 3 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/proof-handling.rst | 7 |
2 files changed, 7 insertions, 3 deletions
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..4a94a5e643 100644 --- a/doc/sphinx/proof-engine/proof-handling.rst +++ b/doc/sphinx/proof-engine/proof-handling.rst @@ -705,9 +705,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 ```````````````````````` |