The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

Does replacing [forall b : A, r (a*b) (P b) _] with [(fun x => forall b : A, r (a*b) (P b) (x b)) _] work (possibly with some additional type annotations)?

-Jason

On Sun, Feb 16, 2014 at 10:46 AM, Anders Lundstedt <anders AT anderslundstedt.se> wrote:

On Sun, Feb 16, 2014 at 8:50 AM, Arnaud Spiwack
<aspiwack AT lix.polytechnique.fr> wrote:
> ... Except moving to the development

> version of Coq: the refine tactic has been completely reimplemented and
> accepts holes anywhere.

Is it possible to just add the reimplented refine tactic as a custom
tactic, without too much fuss?