The Coq mailing list

[Dan Synek <synek AT cs.kun.nl>]

Hi,

This is a part of a tactic I want to wtite:

Ltac Ct F :=
match F with
   true => True
|  false => False
|  (andb ?f1 ?f2) => and (Ct f1) (Ct f2)
end.
I get the following error message:
Error: The reference Ct was not found in the current environment
It seems like Coq does not allow recursive tactics,  but according to 
the manual it does.
What am I doing wrong?
Thanks
Dan