The Coq mailing list

[Abhishek Anand <abhishek.anand.iitg AT gmail.com>]

Yes, I would switch between the 3 buffers.

It would help to make the switching easy in the one-buffer mode.

For example, if the key bound to "company-coq-proof-goto-point" (C-c RET by default) is pressed in a non-code buffer, the code buffer should be switched to.

Also, when that key is pressed in the code buffer, inside a proof or immediately after a query, the proof or the query buffer may be switched to accordingly.

An android user can then assign a convenient key, perhaps even a hardware button (e.g. power button) to trigger "company-coq-proof-goto-point" .

-- Abhishek

http://www.cs.cornell.edu/~aa755/

On Wed, Oct 18, 2017 at 3:51 AM, Pierre Courtieu <pierre.courtieu AT gmail.com> wrote:

Thanks for details,

How would you see the state of your goal in one-buffer mode? Would you
switch between the three buffers?

Pierre