search

ilyasergey / pnp

Lecture notes for a short course on proving/programming in Coq via SSReflect.
https://ilyasergey.net/pnp
BSD 2-Clause "Simplified" License
159 stars 16 forks source link

notation-incompatible-format warnings #23

Open anton-trunov opened 3 years ago

anton-trunov commented 3 years ago

There is a bunch of warnings like this one:

COQC solutions/SsrStyle_solutions.v
File "./solutions/SsrStyle_solutions.v", line 1, characters 0-65:
Warning: Notation "[ rel _ _ : _ | _ ]" was already defined with a different
format in scope fun_scope. [notation-incompatible-format,parsing]

Looks like for Coq 8.12 there is no other solution but disable this warning.