coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Tactic language

From: Quang-Huy Nguyen <Quang-Huy.Nguyen AT loria.fr>
To: coq-club AT pauillac.inria.fr
Subject: [Coq-Club] Tactic language
Date: Thu, 05 Dec 2002 16:28:23 +0100
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

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 ?

Many thanks,

Huy.

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