The Coq mailing list

[Pierre Boutillier <pierre.boutillier AT pps.univ-paris-diderot.fr>]

On 22/04/2013 10:49, Pierre Courtieu wrote:
> Hi, I recently added a feature for this in proofgeneral, and it could
> be very easily added to coqide too. "show ith goal", "Print" and
> "Check" have variants that do that. You can have them by the menu or
> simply add C-u before your usual keybinding.
>
> Adding this kind of queries to coqide would be easy: "Print with
> implicits" "Check without notation".
>  
> For the purpose of a turorial it is probably better to have it in the
> buffer. Adding the same variant directly in Coq syntax would maybe be
> helpful.
I agree that it is very pertinent to choose this for each printing
command. Moreover, implementation of that could have the great side
effect to substitute a lot of imperrative lookup to global references
spread all over the code by a record with configuration passed to
functions ;-).
>
>     I don't like the imposed-by-emacs way of dealing with options.
>
>  
> 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, Are PG users ready for that ? Can I, at last, make these
options asynchronous ?
>
> P.
Pierre B.