The Coq mailing list

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

On Thu, Dec 22, 2005 at 12:20:36PM +0100, Lionel Elie Mamane wrote:

> 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"

I managed to avoid variable capture by doing:

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

That's the idea. But it doesn't work and I don't understand
why. Because this works:

pattern x.
match goal with |- ?foo ?x =>
  pose (O:=foo)
end.
apply K_dec with (P:=O); unfold O;
clear O.

And this doesn't:

pattern x.
match goal with |- ?foo ?x =>
  pose (foo:=foo)
end.

Does someone understand what's happening? The error message I get is:

User error: No matching clauses for match goal
            (use "Debug On" for more info)

-- 
Lionel