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.

  Ltac definitions are used to build tactics but it is convenient and
allowed to define intermediate ltac definitions that just build
terms. Ct above is such a definition.

  On the syntactic side, ltac expressions that return tactics and ltac
expressions that return terms share the same syntactic constructions
("match", "let", juxtaposition as application, ...). Each
subexpressions of these constructions is parsed using a default parser
as indicated in the reference manual. For instance, the branches of a
match expect "expr", i.e. tactic expressions. To return a term when a
tactic is expected, the prefix "constr:" must be given to tell the
parser to choose the right grammar entry.  As an exception, single
identifiers, even those denoting terms, can be given without requiring
"constr:". This is because the role of "constr:" is purely syntactic
and that identifiers of terms and of tactics are treated the same.

  Conversely, when the default is to expect a term (typically
arguments of an applied ltac definitions), the prefix "ltac:" must be
given to tell the parser to select the entry parsing tactic
expressions.

  Hugo