Set Warnings does not reset warnings, one would need to do
Set Warnings "-all,default" to reset.
Set Warnings is actually converted to Set Warnings Append by the implementation, same for Set Debug
Set ... Append "thing" seems undocumented)
Then I don't understand your comment in the PR "The point is that unmentioned warnings are reset, so for instance".
The description of the Warnings flags seems a bit thin. It should mention
Set Warnings "-all,default". It doesn't list or explain the available categories. Readers shouldn't have to experiment or read code to get a full understanding of this flag. Who is the expert on it? Is it still deemed experimental?
I created https://github.com/coq/coq/issues/16963 to cover documenting "Append"
Warnings are not experimental, but I agree there is insufficient documentation. See https://github.com/coq/coq/issues/13557 and the issues and PR linked from there.
Last updated: Jun 09 2023 at 07:01 UTC