diff options
| author | Jim Fehrle | 2019-04-28 12:04:54 -0700 |
|---|---|---|
| committer | Jim Fehrle | 2019-05-16 20:33:41 -0700 |
| commit | 9b41ff4e90a0303d9caf6e7e2f951a5046ce2d13 (patch) | |
| tree | e60ab950f28d2055949f4c9761a09d9030e67797 /CHANGES | |
| parent | 09e099f44b0dc242367eb19d584b941a6dc0de09 (diff) | |
Highlight diffs in goals and some error messages
using Coq's proof diffs feature.
Diffstat (limited to 'CHANGES')
| -rw-r--r-- | CHANGES | 8 |
1 files changed, 5 insertions, 3 deletions
@@ -75,7 +75,6 @@ and the PG Trac http://proofgeneral.inf.ed.ac.uk/trac Hide/ unhide status remains when goal changes. - *** Highlighting of hypothesis You can highlight hypothesis in goals buffer on a per name @@ -84,8 +83,7 @@ and the PG Trac http://proofgeneral.inf.ed.ac.uk/trac Highlighting status remains when goal changes. - -**** Automtic highlighting with (search)About. +**** Automatic highlighting with (search)About. Hypothesis cited in the response buffer after C-c C-a C-a (i.e. M-x coq-SearchAbout) will be highlighted automatically. Any other hypothesis highlighted is unhighlighted. @@ -94,6 +92,10 @@ and the PG Trac http://proofgeneral.inf.ed.ac.uk/trac (setq coq-highlight-hyps-cited-in-response nil) +*** Support Coq's feature for highlighting the differences + between successive proof steps. See section 11.8 ("Showing + Proof Diffs") in the documentation. + *** bug fixes - avoid leaving partial files behind when compilation fails - 123: Parallel background compliation fails to execute some |