coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Implementation of tactics at the OCaml level

From: David Pereira <dpereira AT liacc.up.pt>
To: coq-club AT pauillac.inria.fr
Subject: [Coq-Club] Implementation of tactics at the OCaml level
Date: Tue, 27 Oct 2009 15:13:27 +0000
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

Hi all,

Does anyone know of some simple examples about how to implement coq tactics (version 8.2) directly in OCaml?

Best regards,
David.

David Pereira
MAP-i Phd Student in Computer Science
Researcher at LIACC - UP
Contacts : dpereira_at_liacc_dot_up_dot_pt
(+351)-220402900

[Coq-Club] Implementation of tactics at the OCaml level, David Pereira