The Coq mailing list

[Hugo Herbelin <herbelin AT pauillac.inria.fr>]

  Hi Jasper,

> > Ltac Ct F :=
> >  match F with
> >     true => True
> >  |  false => False
> >  |  (andb ?f1 ?f2) => let c1 := Ct f1 with c2 := Ct f2 in constr:(and
> >  | c1 c2)
> >
> >  end.
> 
> Aren't Ltac definitions supposed to return tactics? After all, True and 
> False are terms, not tactics.

  No, Ltac definitions may return terms (as above) or tactics. As the
parser of expression is distinct from the parser of terms, an explicit
coercion "constr:" has to be inserted to tell that this or this Ltac
expression is actually a term. This keyword is optional though when
the expression is just a qualified identifier (as above for "True" and
"False").

  As an exception, arguments of an Ltac application are parsed by
default as terms, so that a Ltac expression occurring as argument of a
call to a Ltac function must be prefixed by the coercion "ltac:".

  This is shown in the Reference Manual (compare the entry "expr"
which parses tactic expressions and the entry "tacarg" which parses
term expressions).

  Hope it helps.

  Hugo