search

jwiegley / category-theory

An axiom-free formalization of category theory in Coq for personal study and practical work
BSD 3-Clause "New" or "Revised" License
745 stars 68 forks source link

Adapt to coq/coq#15802 #27

Closed proux01 closed 2 years ago

proux01 commented 2 years ago

@jwiegley please merge this at your convenience to avoid warnings in the next Coq 8.16 (to be released this summer) and breakages in future versions (c.f., https://github.com/coq/coq/pull/15802 for the details).

jwiegley commented 2 years ago

@proux01 I guess now is the time to decide whether I give up 8.10-8.13 compatibility...

Blaisorblade commented 2 years ago

If you want to keep compatibility you can use #[global] instead of #[export]. Disabling the warning might also be fine, if the coercions are acceptable.