The Coq mailing list

[Jianzhou Zhao <jianzhou AT seas.upenn.edu>]

I tried

\begin{coq_example*}
Definition f a : Prop := a.
\end{coq_example*}

coq-tex still generated

\begin{flushleft}
\texttt{Coq~{<}~Definition~f~a~:~Prop~:=~a.}\\
\end{flushleft}

Do I need to use any flag?

P.S. Do you know if there is a way to write math symbols in coq example? 
Thanks.

On Mon, May 28, 2012 at 5:12 AM, Arnaud Spiwack
<aspiwack AT lix.polytechnique.fr>
 wrote:
> You can use the environment coq_example*
>
>
> On 26 May 2012 16:50, Jianzhou Zhao 
> <jianzhou AT seas.upenn.edu>
>  wrote:
>>
>> 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
>
>



-- 
Jianzhou