aboutsummaryrefslogtreecommitdiff
path: root/engine
diff options
context:
space:
mode:
authorJim Fehrle2018-08-07 11:59:11 -0700
committerJim Fehrle2018-09-20 13:21:18 -0700
commit2dc65d41b0c3b3481958e1e224fd5ef05f57f243 (patch)
tree76849de729430ee17134fa8993ec7913ec92d321 /engine
parenta828bcedb8ad60c5b1f4cf71f92f24f2c1197ecb (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