The Coq mailing list

[Pierre Courtieu <pierre.courtieu AT gmail.com>]

2013/4/22 Pierre Boutillier <pierre.boutillier AT pps.univ-paris-diderot.fr>

> Nobody seems to know but there is a "Coq" menu in PG :-), with a lot

> of stuff that one can click on *or bind to a shortcut key*. See "Coq
> -> options".

Amazing news

I wouldn't call that a "news", it has been there for a decade (or maybe two) :).

 

Can I, at last, make these
options asynchronous ?

You mean that coq should not toggle them back when backtracking in the buffer? I wouldn't mind but from a user interaction perspective I guess that similar-looking options should behave the same. All "Set/Unset" switchers should be synchronous and let us have a different keyword for asynchronous switchers. Or the other way around ("Toggle" for synchronous, and "Set/Unset" for asynchronous?). And I wouldn't mind having some options with both switchers, unless there is strong design problem... Options for printing for people who prefer that. Except if there is a really good design reason for not having that.

, Are PG users ready for that ?

As I said, nobody seems to be aware of the existence of this menu. So I would say no there are not ready.

For the "imperative lookups" I don't understand your problem: aren't all other options than Printing dealt the same way anyway?

Best regards,

Pierre