The Coq mailing list

[Yves Bertot <Yves.Bertot AT sophia.inria.fr>]

Ryan Rusich wrote:
> Dear All, Can anyone point me in the direction of the documentation for
> extracting natural language from proofs using Coq? I read that it was
> included in Coq from version 6.2 on, but have run into some difficulty
> identifying the name of the command, and the location documentation
> pertaining to it on the Coq website.
> Thank you,
> Ryan
>
>   
If I remember correctly, the support for this command has been 
discontinued.  The best documentation on this capability is documented 
in references 87, 95, 102 of http://www-sop.inria.fr/marelle/projet.html 
(today's version).

We (the Lemme/Marelle team at INRIA Sophia) still have a tool chain that 
produces natural language text from proofs, but it is external to Coq, 
and we definitely have a hard time to maintain it.  It is based on the 
Pcoq system, which is 50% compatible with the newest version of Coq (not 
all tactics are supported, the module system is not, notations are not, 
and so on).

The best references on this work are 47, 70, 71, 81, 87, 90, 92, 95, 
100, 102, 104, 105.

I always dream of putting this software back on public distribution.  It 
has some funny capabilities, but it is hard to maintain.  We used it 
intensively for some of our first big proofs, but we don't anymore: we 
now use proof-general or coqide.

Yves