search

arthuraa / deriving

Class instances for Coq inductive types with little boilerplate
MIT License
24 stars 9 forks source link

Adapt to math-comp/math-comp#1166 #28

Closed pi8027 closed 6 months ago

pi8027 commented 7 months ago

We plan to change the type of the display parameter of the order type structures in order.v (see math-comp/math-comp#1166). This PR provides a compatibility layer.

proux01 commented 6 months ago

@arthuraa upstream PR in mathcomp is now ready for merge. This overlay being backward compatible, could you please merge it so that we can then merge the upstream PR.

arthuraa commented 6 months ago

@pi8027 @proux01 Sorry for the delay!

arthuraa commented 6 months ago

Hm, as far as I can tell, I merged this PR into master, but it is still being displayed as just "closed", rather than "merged"... Any idea about what might have happened?

proux01 commented 6 months ago

Sorry for the delay!

No worries, we are waiting for the upstream PR for maybe a year, so I wouldn't call a few hours a "delay".

Hm, as far as I can tell, I merged this PR into master, but it is still being displayed as just "closed", rather than "merged"... Any idea about what might have happened?

I don't know, apparently some strange interaction with #27 . Anyway, the commits are there on master, that's what counts.

pi8027 commented 6 months ago

No worries, we are waiting for the upstream PR for maybe a year, so I wouldn't call a few hours a "delay".

Actually, I have been waiting for 4 years :-)