The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

I suggest entering "test" code in a regular buffer to run it.  You can 
just undo and delete it right afterward.

Bernard Hurley wrote:
> 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