fix: ghost goals in autoparam tactic block #6408
Merged
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
This PR fixes a regression where goals that don't exist were being displayed. The regression was triggered by #5835 and originally caused by #4926.
Bug originally reported at https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/tactic.20doesn't.20change.20primary.20goal.20state/near/488957772.
The cause of this issue was that #5835 made certain
SourceInfo
s canonical, which was directly transferred to severalTacticInfo
s by #4926. The goal state selection mechanism would then pick up these extraTacticInfo
s.The approach taken by this PR is to ensure that the
SourceInfo
that is being transferred by #4926 is noncanonical.