GAG-MODE

verbosity of proof output
Major Section:  MISCELLANEOUS

Please see set-gag-mode for an explanation of gag-mode, which can take any of the following values:

(gag-mode) ; generally evaluates to t, nil, or :goals