coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Suggestions for Proof General?

From: Jonathan Leivent <jonikelee AT gmail.com>
To: Pierre Courtieu <pierre.courtieu AT gmail.com>, Coq Club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Suggestions for Proof General?
Date: Thu, 23 Jun 2016 12:14:16 -0400
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=jonikelee AT gmail.com; spf=Pass smtp.mailfrom=jonikelee AT gmail.com; spf=None smtp.helo=postmaster AT mail-qk0-f174.google.com
Ironport-phdr: 9a23:QeeJvhZTRTU1au48S7HsWDb/LSx+4OfEezUN459isYplN5qZpM27bnLW6fgltlLVR4KTs6sC0LuO9fi+Ejxaqb+681k6OKRWUBEEjchE1ycBO+WiTXPBEfjxciYhF95DXlI2t1uyMExSBdqsLwaK+i760zceF13FOBZvIaytQ8iJ3pzxj775q8ebSj4LrQL1Wal1IhSyoFeZnegtqqwmFJwMzADUqGBDYeVcyDAgD1uSmxHh+pX4p8Y7oGx48sgs/M9YUKj8Y79wDfkBVGxnYCgJ45jTtBTZVwbHzXwBSHkXnwcAVxDE4QvgU9H6tTbgqutwxQGVOMT3SfY/XjH0q+9ATwagoyMaPXZt+2bOz8d0kahzoRS7phU5zZSCM6+PM/8rXKTbdM8aTGwJestQSSFHHsvobYwJDukMOetVh4b4rloK6xC5AF//V6vU1jZUiyqujuUB2OM7HFSDhVR4Eg==

On 06/23/2016 10:50 AM, Pierre Courtieu wrote:

...
Another remark: In the different standard layouts of PG buffers the goal
window is the "next" window of the scripting window, therefore M-pgup and
M-PgDwn should scroll it page by page. These are standard emacs shortcuts
for functions scroll-other-window and scroll-other-window-down. Note these
function have optional arguments to change the number of lines to scroll.

Hope this helps.

Pierre

Yes, that certainly helps! Thanks for the info!

-- Jonathan

Re: [Coq-Club] Suggestions for Proof General?, (continued)