The Coq mailing list

[Bernard Hurley <bernard AT marcade.biz>]

Hi Edward,

Thanks, I am using emacs because I use it for just about everything!
Besides I have lots of kbd macros defined for various utf8 characters
etc. I only need the *coq* buffer occasionally, e.g. for informally
testing a Fixpoint, so I think I will just have to live with the messy
prompt!

On Fri, 2012-04-06 at 21:39 -0400, Edward Z. Yang wrote:
> 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