The Coq mailing list

[Clément Pit--Claudel <clement.pit AT gmail.com>]

On 03/03/2016 02:23 PM, Ralf Jung wrote:
>> )
> All my experiments with tactics-in-terms lead to the same trouble as
> plain eq_refl: The tactic is run before the contexts are propagated
> down, so things don't work. But it may well be that I did this wrong; I
> have yet to see a successful use of tactics-in-terms ;-)

Something like this?

Definition test2 : expr nil :=
  ltac:(refine (Lam _ "x" (Var _ "x" _)); apply eq_refl).

Attachment: signature.asc
Description: OpenPGP digital signature