The Coq mailing list

[Houda Anoun <anoun AT labri.fr>]

Hi,
I think that the expression (and (Ct f1) (Ct f2)) is not a well formed 
one as it is not allowed by the grammar of the language Ltac. (cf. Coq 
Manual page 168 for more details about the syntax of Ltac)
Otherwise, we can easily write recursive tactics for example the 
following one:

Ltac Ct F :=
match F with
  true => True
|  false => False
|  (andb ?f1 ?f2) =>  (Ct f1)
end.

In your case why do you want to define a tactic? and not a recursive 
function ?
Hope it helps

Houda

Dan Synek wrote:

> 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
>
> --------------------------------------------------------
> Bug reports: http://coq.inria.fr/bin/coq-bugs
> Archives: http://pauillac.inria.fr/pipermail/coq-club
>          http://pauillac.inria.fr/bin/wilma/coq-club
> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club


--
==============================
|      Houda ANOUN           |
|         LaBRI              |
| 351 Cours de la libération |
|      33405 Talence         |
|    phone: 0540002489       |
|  e-mail 
:anoun AT labri.fr
    |
=============================