The Coq mailing list

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

  Hi Dan,

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

  This is because Ltac subexpressions (to the exception of variables)
are not allowed as part of Coq term expressions. You have to use
"let"'s as follows:

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.

  Best regards,

  Hugo