The Coq mailing list

[Adam Chlipala <adam AT chlipala.net>]

Aaron Bohannon wrote:
> Why do the first four definitions succeed while the fifth one fails?
> (I have a very hard time imagining I'm the first to discover this...)
>
> Ltac t := t.
>
> Ltac t := t t.
>
> Ltac t u := t u.
>
> Ltac t u := t t u.
>
> Ltac t u := t (t u).
> Error: The reference t was not found in the current environment.
>    

Two main parsing non-terminals are used in Ltac: "ltac" (tactic code) 
and "constr" (Gallina code).  By default, the body of a tactic 
definition is "ltac," while the arguments to tactic functions are 
"constr."  You can usually switch non-terminals using the notation 
demonstrated below:
    Ltac t u := t ltac:(t u).

I'm not sure if this will work dynamically.  I usually [let]-bind tactic 
calls whose results will be passed to other tactics.