diff options
| author | Jim Fehrle | 2018-08-07 11:59:11 -0700 |
|---|---|---|
| committer | Jim Fehrle | 2018-09-20 13:21:18 -0700 |
| commit | 2dc65d41b0c3b3481958e1e224fd5ef05f57f243 (patch) | |
| tree | 76849de729430ee17134fa8993ec7913ec92d321 /engine | |
| parent | a828bcedb8ad60c5b1f4cf71f92f24f2c1197ecb (diff) | |
Current diff code only compares the first current goal of the old and new
proof states. That's not always correct. This change will a) show diffs
for all displayed goals and b) correctly match goals between the old and
new proof states.
For example, "split." will show diffs for both resulting goals.
"all: swap 1 2" will show the same diffs as for the old proof state, though
in a different position in the output.
Please see comments before Proof_diffs.make_goal_map_i and Proof_diffs.match_goals
for a description of how goals are matched between old and new proofs.
Diffstat (limited to 'engine')
0 files changed, 0 insertions, 0 deletions
