diff options
| -rw-r--r-- | checker/mod_checking.ml | 2 | ||||
| -rw-r--r-- | doc/changelog/12-misc/10019-PG-proof-diffs.rst | 3 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/proof-handling.rst | 7 |
3 files changed, 8 insertions, 4 deletions
diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml index dedbddfee0..ccce0bd9a7 100644 --- a/checker/mod_checking.ml +++ b/checker/mod_checking.ml @@ -23,7 +23,7 @@ let check_constant_declaration env kn cb = (* [env'] contains De Bruijn universe variables *) let poly, env' = match cb.const_universes with - | Monomorphic ctx -> false, push_context_set ~strict:true ctx env + | Monomorphic ctx -> false, env | Polymorphic auctx -> let ctx = Univ.AUContext.repr auctx in let env = push_context ~strict:false ctx env in 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 ca7f037815..0cff987a27 100644 --- a/doc/sphinx/proof-engine/proof-handling.rst +++ b/doc/sphinx/proof-engine/proof-handling.rst @@ -692,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 ```````````````````````` |