coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: Pierre Courtieu <pierre.courtieu AT gmail.com>
To: Coq Club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Suggestions for Proof General?
Date: Thu, 23 Jun 2016 23:06:57 +0200
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=pierre.courtieu AT gmail.com; spf=Pass smtp.mailfrom=pierre.courtieu AT gmail.com; spf=None smtp.helo=postmaster AT mail-lf0-f54.google.com
Ironport-phdr: 9a23:r96JBBXjspS2p8y/TgbxzWaP3AbV8LGtZVwlr6E/grcLSJyIuqrYZhOGt8tkgFKBZ4jH8fUM07OQ6PG4HzRfqs7c+Fk5M7V0HycfjssXmwFySOWkMmbcaMDQUiohAc5ZX0Vk9XzoeWJcGcL5ekGA6ibqtW1aJBzzOEJPK/jvHcaK1oLshrj0o8KYO1gArQH+SIs6FA+xowTVu5teqqpZAYF19CH0pGBVcf9d32JiKAHbtR/94sCt4MwrqHwI6LoJvvRNWqTifqk+UacQTHF/azh0t4XXskzoShLHzX8BWC1CmR1RRgPB8RvSX5HrsyK8uPAriweAOsijdbE5Qy6vp4xsVQX0iSoaf2oh8WzNkME2h6VGug6gqgFXzIvdYYXTP/17KPCONegGTHZMC54CHxdKBZmxOs5WV7IM

2016-06-23 22:51 GMT+02:00 Jonathan Leivent <jonikelee AT gmail.com>:

On 06/23/2016 04:37 PM, Ralf Jung wrote:

Hi,

In a really long telescope, would it make sense to be able to see the beginning and the end, with the middle initially hidden?
Maybe another opportunity for hide-show? So that the goal would look like this initially:

======
P1 -> ... P

with the ability to show more info on the left by clicking?

-- Jonathan

Why not.

Ideally hypothesis would go in a different subwindow than the conclusion anyway, so that scrolling in the hyps does not hide or move the goal.

Then telescope being yet another set of hypothesis (cf R. Krebbers proof mode), they would go in yet another window?

Leading to something like:

H1:... scrollable

H2: ..

================

P2 scrollable

----------------

P scrollable

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