The Coq mailing list

[Christian Doczkal <christian.doczkal AT ens-lyon.fr>]

Hello,

That was indeed very helpful. Maybe the manual could be improved to more
clearly state the connection between the printed messages and the
command-line switches.

Somewhat related, there are other warnings (e.g., "Warning: Noting to
inject.") that predate the current warning system and seem to be
unaffected by any warning switches. Is there a way to turn the
aforementioned waring off or into an error?

Best,
Christian


Is there also a way for turning "Warning: Nothing to Inject" into a
On 11/05/2017 12:16 PM, Théo Zimmermann 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
>  
> <mailto: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
>