The Coq mailing list

[Christian Doczkal <doczkal AT ps.uni-sb.de>]

(* Sorry for my previous incomplete message! *)

Hello Everyone

>From what I read so far, there seem to be a number of different ways to
extend Coq with additional tactics. 

     1. Code it directly in Ltac
     2. Use reflection and code it directly in Gallina
     3. Code an external tactic and call it using "external" using XML
        for communication
     4. Coding the tactic directly into Coq at the OCaml level

1 and 2 are covered to some extent in the Coq Reference Manual and in
Adam Chlipala's cpdt notes. Is there any documentation available how to
get started with coding tactics using variant 3 and/or 4? (Besides
browsing the Coq source files)

Does someone have short nicely documented .ml file of a simple tactic
for demonstration purposes?

-- 
Regards
Christian