The Coq mailing list

[Jasper Stein <J.Stein AT cs.ru.nl>]

Hello Hugo,

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

Am I missing something?

Jasper
-- 
The problem with having an open mind is that people toss in garbage