summaryrefslogtreecommitdiff
path: root/test-suite/bugs/opened/3410.v
blob: 0d259181aa56c5c35ec6e00386e3ff1fb5b0308b (plain)
1
Fail repeat match goal with H:_ |- _ => setoid_rewrite X in H end.