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 for a new rapply tactic #78

Closed JasonGross closed 1 year ago

JasonGross commented 5 years ago

This backwards compatible change makes math-classes work with coq/coq#10760 by replacing all instances of rapply which were relying on typeclass resolution happening before refine (instead of simultaneously with it) to instead invoke Tactics.rapply (which is the same tactic in Coq <= 8.10, and which will be the tactic rather than the uconstr-taking tactic notation in Coq >= 8.11).

See also https://github.com/coq/coq/pull/10760#issuecomment-532399518

For reference, this changes 9 of the 34 invocations of rapply.

Zimmi48 commented 5 years ago

Note that while this patch does no harm, it is not clear yet whether coq/coq#10760 will be merged as is, and thus whether it will be necessary.

spitters commented 5 years ago

I'm fine with the changes, but propose to wait until the discussion in coq/coq#10760 stabilizes.