coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: Clément Pit--Claudel <clement.pit AT gmail.com>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Suggestions for Proof General?
Date: Fri, 17 Jun 2016 22:23:16 -0400
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=clement.pit AT gmail.com; spf=SoftFail smtp.mailfrom=clement.pit AT gmail.com; spf=None smtp.helo=postmaster AT mout.kundenserver.de
Ironport-phdr: 9a23:ntUZIhf9Pa/b5yaqKzPZLZnMlGMj4u6mDksu8pMizoh2WeGdxc6+YR7h7PlgxGXEQZ/co6odzbGG4uaxACddsd6oizMrTt9lb1c9k8IYnggtUoauKHbQC7rUVRE8B9lIT1R//nu2YgB/Ecf6YEDO8DXptWZBUiv2OQc9HOnpAIma153xjLDjvcyKKFgYzBOGIppMbzyO5T3LsccXhYYwYo0Q8TDu5kVyRuJN2GlzLkiSlRuvru25/Zpk7jgC86l5r50IAu3GePEzSqUdBzA7OUg04tfqvF/NV1ih/HwZB04SEx9FBRTy1BDmG9LatiLnuud5kH2ROcDzQLYoHyyj849kTRbpjGEMMDtvozKfsdB5kK8O+EHpnBd42YOBOIw=

On 2016-06-17 19:02, John Wiegley wrote:
>>>>>> Jonathan Leivent
>>>>>> <jonikelee AT gmail.com>
>>>>>> writes:
>
>> Could PG be made to show multiple complete goals if the goal window is big
>> enough?
>
> I'd like it if I could just always make sure that the top of the current
> goal
> is brought into view after each command. I find myself manually scrolling
> the
> response window often when large goals are involved.

Please file a bug report: this is already implemented, I think, so you're
most likely running into a bug :)

Attachment: signature.asc
Description: OpenPGP digital signature

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