https://github.com/coq/coq/pull/16902#discussion_r1043649768
@Jim Fehrle
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
(btw 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: Sep 30 2023 at 16:01 UTC