coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] How to remove "Coq <" from coq-tex's output

From: Julien Tesson <julien.tesson AT univ-orleans.fr>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] How to remove "Coq <" from coq-tex's output
Date: Wed, 30 May 2012 17:56:45 +0900

Le 26/05/2012 23:50, Jianzhou Zhao a écrit :
> Hi,
>
> The output of coq-tex is by default started with "Coq <" at the
> beginning of each line. Is there a way to remove "Coq <"? Thanks.
>

Hi,

I have a modified version of coq-tex which make the output result much more
flexible by encapsulating the resulting latex code in latex commands and
environments that you can redefine.
It is available here
http://tesson.julien.free.fr/research/projects/coqtex/index.php
You need to have the coq sources to install it.

I hope it can help.
Sincerely,
Julien

--
Julien Tesson, Postdoctoral researcher
Kochi University of Technology, Japan
http://tesson.julien.free.fr/?lang=en

[Coq-Club] How to remove "Coq <" from coq-tex's output, Jianzhou Zhao, 05/26/2012
- Re: [Coq-Club] How to remove "Coq <" from coq-tex's output, Arnaud Spiwack, 05/28/2012
  - Re: [Coq-Club] How to remove "Coq <" from coq-tex's output, Jianzhou Zhao, 05/29/2012
    - Re: [Coq-Club] How to remove "Coq <" from coq-tex's output, Arnaud Spiwack, 05/30/2012
- Re: [Coq-Club] How to remove "Coq <" from coq-tex's output, Julien Tesson, 05/30/2012
- Re: [Coq-Club] How to remove "Coq <" from coq-tex's output, Mehdi Dogguy, 05/30/2012