The Coq mailing list

[Erkki Luuk <erkkil AT gmail.com>]

Thanks for the info.. (didn't solve my problem, though -- https://github.com/coq/coq/issues/6068#issuecomment-341942935)

Erkki

On Sun, Nov 5, 2017 at 1:16 PM, Théo Zimmermann <theo.zimmi AT gmail.com> wrote:

Hi,

Section 6.9.3 (https://coq.inria.fr/distrib/current/refman/vernacular.html#SetWarnings) also says "Adding - in front of a warning or category disables it, adding + makes it an error. It is possible to use the special categories all and default, the latter containing the warnings enabled by default."

The warnings names and categories are displayed whenever you see such a warning (I ignore if there is a command to display all warning names or categories).

E.g. if you type "Variable A : Prop." in an empty buffer, you will see:
"A is declared as a local axiom [local-declaration,scope]"

The warning name is local-declaration and the category is scope.

Thus if you relaunch CoqIDE (or coqtop through Proof-General) with option -w "-local-declaration", you won't see any warning for the same buffer.

And if you use option -w "+local-declaration", you will see an error instead.

Théo

Le sam. 4 nov. 2017 à 23:27, Erkki Luuk <erkkil AT gmail.com> a écrit :

Hi

Where do I find the command line flags for warning names and categories? The manual just says:

-w (all|none|w1,…,wn)

Configure the display of warnings. This option expects all, none or a comma-separated list of warning names or categories (see Section 6.9.3).

https://coq.inria.fr/distrib/current/refman/commands.html#hevea_default978

Erkki