Errors make too many nodes obsolete
- Have the IDE open
- In your favorite editor, edit the code of a function but make a syntax or type error
- Reload, the IDE shows the error and a ton of detached nodes
- Fix the error
Expected results: obsolete nodes are the same as if the change was made without error (so the subgoals after the change in the function)
Actual result: every node in the proof is obsolete, even those outside the modified function
This gets old very fast in proofs that take a lot of time to replay.