coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Tactic language

From: Jean-Christophe Filliatre <Jean-Christophe.Filliatre AT lri.fr>
To: Quang-Huy.Nguyen AT loria.fr
Cc: coq-club AT pauillac.inria.fr
Subject: Re: [Coq-Club] Tactic language
Date: Thu, 5 Dec 2002 16:51:03 +0100
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

Quang-Huy Nguyen writes:
> Hi,
>
> I have a question related to the tactic language (Chapter 10 of the
> manual).
>
> What are exactly the tactics that can be used in a definition by this
> language ?
> Can I call a tactic developed in OCaml in such a definition ?

Yes you can call any tactic. The syntax for tactic expressions in the
tactic language is the same as when entered directly within a proof.

--
Jean-Christophe

[Coq-Club] Tactic language, Quang-Huy Nguyen
- Re: [Coq-Club] Tactic language, Jean-Christophe Filliatre