From 5ec7eca640a6ee495eb2c0fb8d8a4076256ff96d Mon Sep 17 00:00:00 2001 From: Jim Fehrle Date: Sat, 6 Jul 2019 19:25:39 -0700 Subject: Show diffs in "Show Proof." Add experimental "Show Proof" command to the toplevel that shadows the current command in the parser (in coqtop and PG only). Apply existing code to highlight diffs in the output --- doc/changelog/07-commands-and-options/10494-diffs-in-show-proof.rst | 6 ++++++ 1 file changed, 6 insertions(+) create mode 100644 doc/changelog/07-commands-and-options/10494-diffs-in-show-proof.rst (limited to 'doc/changelog') diff --git a/doc/changelog/07-commands-and-options/10494-diffs-in-show-proof.rst b/doc/changelog/07-commands-and-options/10494-diffs-in-show-proof.rst new file mode 100644 index 0000000000..c1df728c5c --- /dev/null +++ b/doc/changelog/07-commands-and-options/10494-diffs-in-show-proof.rst @@ -0,0 +1,6 @@ +- Optionally highlight the differences between successive proof steps in the + :cmd:`Show Proof` command. Experimental; only available in coqtop + and Proof General for now, may be supported in other IDEs + in the future. + (`#10494 `_, + by Jim Fehrle). -- cgit v1.2.3