Compile with `-w "+compatibility-notation"

coq-community / math-classes

A library of abstract interfaces for mathematical structures in Coq [maintainer=@spitters,@Lysxia]

https://math-classes.github.io

MIT License

162 stars 43 forks source link

Compile with `-w "+compatibility-notation" #63

Closed Zimmi48 closed 6 years ago

Zimmi48 commented 6 years ago

This project should be able to compile with -w "+compatibility-notation" to prepare for the Coq 8.9 release. See also https://github.com/coq/coq/issues/8383.

spitters commented 6 years ago

A better way would be a cleaner stdlib, as started by @ejgallego https://github.com/HoTT/HoTT/issues/795 I know there has been progress on this. I just remember any time now...

Zimmi48 commented 6 years ago

Are you sure you meant to reply here and not at https://github.com/HoTT/HoTT/issues/954?