diff options
| author | Pierre Courtieu | 2019-05-23 09:40:01 +0200 |
|---|---|---|
| committer | GitHub | 2019-05-23 09:40:01 +0200 |
| commit | 0058999ac42d7d1b3ee093aa5a4e8956d1eb8a9c (patch) | |
| tree | a24fc4fa9efd548355945b6595ec4d79fa7373cd /CHANGES | |
| parent | 5bdff05885b29be35962fb06b0339cdd34db1079 (diff) | |
| parent | 7501326a228a5d0af1ad1d5bef4e8640cbd1e43f (diff) | |
Merge pull request #421 from jfehrle/for_master2
Support Coq's proof diffs feature: highlight diffs in goals and some error messages
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 |