coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Jianzhou Zhao <jianzhou AT seas.upenn.edu>
- To: coq-club <coq-club AT inria.fr>
- Subject: [Coq-Club] How to remove "Coq <" from coq-tex's output
- Date: Sat, 26 May 2012 10:50:46 -0400
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.
--
Jianzhou
- [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, Jianzhou Zhao, 05/29/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
- Re: [Coq-Club] How to remove "Coq <" from coq-tex's output, Arnaud Spiwack, 05/28/2012
Archive powered by MHonArc 2.6.18.