The Coq mailing list

[Clément Pit--Claudel <clement.pit AT gmail.com>]

Hi Scott,

PG 4.2 is from 2012; can you try reproducing the issue with 4.4pre? 
https://github.com/ProofGeneral/PG

Clément.

On 02/19/2016 09:39 AM, scott constable wrote:
> Hi All,
> 
> I've been having some trouble with CoqIDE on OSX, so I decided to give PG a 
> try instead. I followed the directions from Lance Pollard here:
> 
> http://lancejpollard.github.io/how-to-install-coq-on-a-mac/
> 
> Everything is working fine so far, except that with every proof step, the 
> goal window grows, and the response window shrinks. I have the 
> proof-three-window-enable option on, which according to the PG manual "also 
> prevents Emacs automatically resizing windows between proof steps." But 
> this doesn't seem to be working properly. Is this a bug? If so, would the 
> problem be with PG or with Aquamacs?
> 
> What follows is my software platform:
> OSX 10.11.3
> Aquamacs 3.2
> PG 4.2
> Coq 8.5
> 
> Thanks in advance,
> 
> ~Scott Constable

Attachment: signature.asc
Description: OpenPGP digital signature