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

Adapt w.r.t. coq/coq#17564. #117

Closed ppedrot closed 1 year ago

ppedrot commented 1 year ago

Should be backwards compatible. The lines tweaked seemed to be precisely workarounds to case unification issues, so it looks like coq/coq#17564 is actually fixing a bug there.