coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] print coq proof states?

From: Adam Chlipala <adamc AT csail.mit.edu>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] print coq proof states?
Date: Thu, 21 Nov 2013 13:51:38 -0500

On 11/21/2013 01:32 PM, Kristopher Micinski wrote:

Didn't Adam Chlipala have a similar set of problems for this when
assembling CPDT, from a post a while back? I remember his soliciting
volunteers to improve coq-tex: I wonder if anyone knows wether that
went anywhere..

I only handled the (relatively infrequent) rendered proof states in CPDT by copying and pasting them, and coqdoc didn't need many changes at all to render them nicely. The changes I needed in coqdoc were mostly about genuine vernacular/Gallina/Ltac code.

[Coq-Club] print coq proof states?, Altenkirch Thorsten, 11/19/2013
- Re: [Coq-Club] print coq proof states?, Nuno Gaspar, 11/20/2013
  - Re: [Coq-Club] print coq proof states?, Altenkirch Thorsten, 11/21/2013
    - Re: [Coq-Club] print coq proof states?, Abhishek Anand, 11/21/2013
    - Re: [Coq-Club] print coq proof states?, Matthieu Sozeau, 11/21/2013
    - Re: [Coq-Club] print coq proof states?, Daniel Schepler, 11/21/2013
      - Re: [Coq-Club] print coq proof states?, Kristopher Micinski, 11/21/2013
        
        Re: [Coq-Club] print coq proof states?, Adam Chlipala, 11/21/2013