coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Coq and RSI

From: Joseph Tassarotti <tassarotti AT college.harvard.edu>
To: Thomas Braibant <thomas.braibant AT gmail.com>
Cc: Pierre Courtieu <pierre.courtieu AT gmail.com>, coq-club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Coq and RSI
Date: Wed, 29 Aug 2012 16:04:59 -0400

Electric terminator do not work when one uses modules ("apply
Foo.lemma"). BTW, when doing go forward at the end of a line that ends
with a period, pg moves the cursor to the next line, which is most
often not what I want it to do (I want to fill this damn line, not to
use one single tactic per line!).

If I understand correctly, this bug with electric terminator has been fixed in the newest version of proof general. See
http://zermelo.dcs.ed.ac.uk/trac/ticket/377 for more details and a temporary fix.

[Coq-Club] Coq and RSI, Thomas Braibant, 08/28/2012
- Re: [Coq-Club] Coq and RSI, Kristopher Micinski, 08/28/2012
- Re: [Coq-Club] Coq and RSI, Enrico Tassi, 08/28/2012
- Re: [Coq-Club] Coq and RSI, J. Ian Johnson, 08/28/2012
  - Re: [Coq-Club] Coq and RSI, Stefan Monnier, 08/28/2012
- Re: [Coq-Club] Coq and RSI, Pierre Courtieu, 08/29/2012
- <Possible follow-up(s)>
- Re: [Coq-Club] Coq and RSI, J. Ian Johnson, 08/28/2012
  - Re: [Coq-Club] Coq and RSI, Pierre Courtieu, 08/29/2012
    - Re: [Coq-Club] Coq and RSI, Thomas Braibant, 08/29/2012
      - Re: [Coq-Club] Coq and RSI, Joseph Tassarotti, 08/29/2012
      - Re: [Coq-Club] Coq and RSI, Pierre Courtieu, 08/30/2012