Skip to Content.
Sympa Menu

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

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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


Chronological Thread 
  • From: Arnaud Spiwack <aspiwack AT lix.polytechnique.fr>
  • To: Jianzhou Zhao <jianzhou AT seas.upenn.edu>
  • Cc: coq-club <coq-club AT inria.fr>
  • Subject: Re: [Coq-Club] How to remove "Coq <" from coq-tex's output
  • Date: Wed, 30 May 2012 14:16:02 +0200


Do I need to use any flag?

No, that's my mistake. Mehdi's solution probably the easiest, I'm afraid
 
P.S. Do you know if there is a way to write math symbols in coq example? Thanks.

I don't think there is. Coq-tex does not have a main maintainer at present time, it does not really evolve, and is lacking many features.




Archive powered by MHonArc 2.6.18.

Top of Page