The Coq mailing list

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

You can make it look a bit cleaner with a notation, too:

Tactic Notation "!!" uconstr(term) :=
  refine term; solve [apply eq_refl].

Definition test2 : expr nil :=
  ltac:(!! (Lam _ "x" (Var _ "x" _))).

Clément.

On 03/03/2016 02:26 PM, Clément Pit--Claudel wrote:
> 
> 
> 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