Commit 2025-10-31 10:48 2ba365e7

View on Github →

fix(TacticAnalysis): remove syntax range check (#28950) In #28802 we discovered the tactic analysis framework does not fire on declarations using where clauses. The reason is that def foo where ... gets turned into def foo := { ... }, and the { ... } syntax is assigned a range outside of the where ... syntax; this causes the syntax range check to omit the whole declaration body. Moreover, Verso involves pieces of syntax without any range at all. So the range of a piece of syntax is essentially meaningless and we should not check it at all.

Estimated changes