The Coq mailing list

[Benjamin Werner <benjamin.werner AT inria.fr>]

Hi,

coq-tex should be the best, if I understand correctly what you
want to do.

Maybye what you are missing is the undocumented
coq_example# environement, which executes the commands
but only prints the result in the *.v.tex file.

So together  with coq_eval, coq_example and coq_example*
you have the four possible behaviours.

I think I am responsible for having added the mode but not the
documentation years ago.

Cheers,

Benjamin



Le 18 sept. 07 à 16:40, Thorsten Altenkirch a écrit :

> Hi everybody,
>
> I am preparing some lecture notes using latex and I'd like to explain
> some coq proofs, displaying the changing proof state in my notes. Is
> there any tool support for this? It seems that neither coqdoc or
> coq-tex are up to the job.
>
> Obviously, it is rather doubtful whether paper is the best way to
> present a proof and maybe one should step through a proof using coqide
> and diplay the comments in a different window. However, for the moment
> I'd be happy if there is an easy way to avoid lots of ugly verbatims
> in my notes.
>
> Cheers,
> Thorsten
>
>
> This message has been checked for viruses but the contents of an  
> attachment
> may still contain software viruses, which could damage your  
> computer system:
> you are advised to perform your own checks. Email communications  
> with the
> University of Nottingham may be monitored as permitted by UK  
> legislation.
>
> --------------------------------------------------------
> Bug reports: http://logical.futurs.inria.fr/coq-bugs
> Archives: http://pauillac.inria.fr/pipermail/coq-club
>          http://pauillac.inria.fr/bin/wilma/coq-club
> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club