The Coq mailing list

[Lionel Elie Mamane <lionel AT mamane.lu>]

Hi,

Ltac seems to protect me from variable capture. Is there any way to
achieve variable capture when one wants it?

E.g. if my current goal is "f x", if I do:

 match goal with |- ?foo =>
  apply K_dec with (P:=fun x => foo)
 end.

Then P gets instantiated with "fun y => f x", but I want it to be
instantiated by "fun x => f x". Is that possible?

(imagine I have a very big expression I don't want to retype instead
of just "f")

-- 
Lionel