Since recently I'm getting annoying warnings in the compilation version compatibility files
e.g.
File "./Coq816.v", line 13, characters 0-33:
Warning: Trying to mask the absolute name "Coq.Lists.ListSet"!
[masking-absolute-name,deprecated]
any idea of the root cause?
I don't get these
Oh wait I just got them
Most likely candidate is #16945
or #16926
tho indeed we don't seem to compile the stdlib with -warn-error
Emilio Jesús Gallego Arias said:
tho indeed we don't seem to compile the stdlib with -warn-error
we do AFAICT at least in dev mode
I used a deprecated thing in Datatypes.v and got
coqc theories/Init/Datatypes.{glob,vo,vos} (exit 1)
File "./Datatypes.v", line 516, characters 18-29:
Error: Notation prodT_curry is deprecated since 8.13. Use uncurry instead.
[deprecated-syntactic-definition,deprecated]
problem is coq817.v restores the warnings by doing Global Set Warnings "masking-absolute-name".
https://github.com/coq/coq/pull/17000
Last updated: Oct 13 2024 at 01:02 UTC