Skip to content

[Merged by Bors] - chore: use skip instead of -failIfUnchanged in the default tactic of Homeomorph#39758

Closed
gasparattila wants to merge 1 commit into
leanprover-community:masterfrom
gasparattila:homeomorph-tactic-skip
Closed

[Merged by Bors] - chore: use skip instead of -failIfUnchanged in the default tactic of Homeomorph#39758
gasparattila wants to merge 1 commit into
leanprover-community:masterfrom
gasparattila:homeomorph-tactic-skip

Commits

Commits on May 23, 2026