search

math-comp / multinomials

Multinomials for the Mathematical Components library.
Other
14 stars 12 forks source link

Adapt to https://github.com/math-comp/math-comp/pull/1031 #81

Closed proux01 closed 1 year ago

CohenCyril commented 1 year ago

I'm afraid this conflicts a bit with #80 which performs a huge cleanup, and which I was about to review and probably merge. @pi8027 @proux01 how would you prefer to handle this?

proux01 commented 1 year ago

@CohenCyril note that this actually is a single char change: https://github.com/math-comp/multinomials/pull/81/commits/48aef729500c92cbb7541b5c2eeb9350add675f3

The actual question is the interaction between #80 and #42 If #80 is merged rapidly, I'm fine rebasing #42 on top of it, otheriwse I really think we shouldn't wait too much to merge the HB port now that MC 2 is out (not having multinomials means not having CoqEAL which makes MC2 not yet usable for many users). Maybe the best solution is to merge #42 now and rebase #80 (I can help if needed but this should be relatively easy from what I can see, it doesn't seem to really touch the structures).