The Coq mailing list

["Robert R. Schneck" <schneck AT math.berkeley.edu>]

In Coq V7, "Load" is very quiet indeed; I remember in 6.3.1 one would
still see "foo is assumed/bar is defined" and so forth.  "Load Verbose"
says too much though.  Is there any way to get the old semi-verbose
behavior?

Also, can someone explain to me the differences between the tactics
EAuto and Prolog?  Such as goals which one can prove but not the other?

Many thanks,
Robert