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

Fix performance bug #96

Closed mattam82 closed 3 years ago

mattam82 commented 3 years ago

The library was crucially missing some Params declarations, resulting in simple rewrites that could take seconds to perform. This is worsened by the upcoming PR coq/coq#13969 which (correctly) infers more sensible default morphism declarations for parts of the goals that are not affected by a rewrite, resulting in even longer proof search. This should be backwards compatible and also a net improvement in performance.

spitters commented 3 years ago

Thanks!