The Coq mailing list

[Edsko de Vries <devriese AT cs.tcd.ie>]

Hi,

First of all, I would like to thank you for writing and supporting Coq.
I have been learning how to use it for while now, and I really like
working with it. I have two questions:

(1) Is there any documentation (a tutorial would be good) on writing
         tactics in O'Caml? I have found
         http://cocorico.cs.ru.nl/coqwiki/CoqCustomizationHowTo, but that is
         very incomplete. I realise there are examples in the contrib/
         directory of the Coq distribution, but they are all very complex.
         (I am trying to write a tactic that can automatically solve a goal
         such as a >= b, where there is a hypothesis of the form ... a + ...
         >= ... + b + ...; I've tried to write it in Ltac but it's not easy -
         at least, not for me :)

(2) Is there a tool that can export a Coq script to human readable form?
         I know that there is coqtex, and that's quite good if you want to
         typeset the theorems without the proofs. However, proofs in Coq are
         very much a dialogue, and reading the proof script is much like
         hearing something talking on a phone without hearing the other
         party. It'd be nice to be able to record the dialogue between both
         parties.

Thanks!

Edsko