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
744 stars 68 forks source link

Use #[export] rather than #[global] in almost all modules #89

Closed jwiegley closed 1 year ago

jwiegley commented 1 year ago

Note that this change will require more imports in user code than previously, but since exports weren't well documented, the pain of this change should result in more future-proof user code.