The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

I believe it's called [rewrite_strat] (or is it actually [strat_rewrite]?), and is present in 8.4, but lacking some features and polish, and is more featurefull in 8.5.

On Sat, Jan 31, 2015 at 2:04 PM, Gregory Malecha <gmalecha AT cs.harvard.edu> wrote:

Hello --

Is there an implementation of autorewrite that will rewrite under binders the way that setoid_rewrite does?

Thank you.

--

gregory malecha

http://www.people.fas.harvard.edu/~gmalecha/