The Coq mailing list

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

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

Hi,
I give you the reasons, I don't argue for them. It can be discussed.

On 22/04/2013 09:14, Gert Smolka wrote:
  The commands are quite useful when explaining Coq to beginners.  For instance, in the lecture notes we more than once have

Set Printing All.
Check TERM.
Unset Printing All.

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 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".

P.