Stream: Coq devs & plugin devs

Topic: stage of warnings option

Gaëtan Gilbert (Sep 05 2023 at 10:23):

Currently Warnings is in Interp stage, but some warnings are at synterp time so this seems incorrect
Would there be problems in moving it to synterp stage?

Last updated: Nov 29 2023 at 22:01 UTC