The Coq mailing list

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

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 "external2 using XML
        for communication
     4. Coding the tactic directly into Coq at the OCaml level