search

coq-community / coq-ext-lib

A library of Coq definitions, theorems, and tactics. [maintainers=@gmalecha,@liyishuai]
https://coq-community.org/coq-ext-lib/
BSD 2-Clause "Simplified" License
129 stars 46 forks source link

rwHyps stops on first recursive equality #144

Open Janno opened 8 months ago

Janno commented 8 months ago

rwHyps changed in https://github.com/coq-community/coq-ext-lib/pull/119 and now stops on the first recursive equality it finds instead of rewriting the remaining (non-recursive) ones.