coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Pierre Courtieu <Pierre.Courtieu AT sophia.inria.fr>
- To: S�bastien Hinderer <Sebastien.Hinderer AT ens-lyon.fr>
- Cc: Coq <coq-club AT pauillac.inria.fr>
- Subject: Re: [Coq-Club] -emacs
- Date: Thu, 19 Jun 2003 11:03:55 +0200
- List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
Sébastien Hinderer
<Sebastien.Hinderer AT ens-lyon.fr>
wrote:
> Hello dear all,
>
> I wonder in which way the "-emacs" command-line argument modifies the
> behaviour of coqtop.
> Thank you very much for answering my question.
> Sébastien.
Hello,
It tells Coq to put the prompt inside some extra special characters,
which allows ProofGeneral to detect it easily.
Pierre
- [Coq-Club] -emacs, Sébastien Hinderer
- Re: [Coq-Club] -emacs, Pierre Courtieu
Archive powered by MhonArc 2.6.16.