The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

Hi,

Is there a variant of [cbv] or of [simpl] (or something) that performs eta reduction?  I'm looking for a built-in version of something like

Ltac eta_red :=

  repeat match goal with

           | [ H : appcontext[fun x => ?f x] |- _ ] => change (fun x => f x) with f in H

           | [ |- appcontext[fun x => ?f x] ] => change (fun x => f x) with f

         end.

(except it would be nice to allow [f] to reference things that are not free in [H]/the goal)

Thanks.

-Jason