The Coq mailing list

["Edward Z. Yang" <ezyang AT mit.edu>]

Hello Benard,

You can use the 'coqtop' executable directly, which will give a nicer
prompt.  Unfortunately, ProofGeneral needs this gunk because it needs
to parse out goal information (so it passes -emacs-U to the process.)

Edward

Excerpts from bernard's message of Fri Apr 06 21:14:47 -0400 2012:
> Hi all,
> 
> I am using coq with prof-general in emacs.  In the *coq* buffer the prompt
> looks like:
> 
> <prompt>Coq < 25 || 0 < </prompt>
> 
> What can I do to clean it up?
> 
> Thanks,
> 
> Bernard