search

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

Remove the few instances of non-global hint declarations. #126

Closed ppedrot closed 7 months ago

ppedrot commented 7 months ago

These commands are fragile and trigger a warning.