The Coq mailing list

[Gert Smolka <smolka AT ps.uni-saarland.de>]

At Saarland University we are teaching Coq in the Intro to Computational 
Logic course.  Since most student don't know Emacs at this point we recommend 
CoqIDE.  When I checked out CoqIDE on MacOs for the first lecture I was 
surprised to get the warning

   Warning: query commands should not be inserted in scripts

for commands like Check, Print, and Compute.  Even worse, the command "Set 
Printing All" is rejected and I get

   Error: Use CoqIDE display menu instead

I don't understand the motivation behind this.  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.

I know that I can do Set and Unset through the display menu.  BTW, Compute is 
missing in the Queries menu.

Gert