Port to Hierarchy Builder

[proux01]

No description provided.

[proux01]

@CohenCyril CI is as green as it can be

[CohenCyril]

@CohenCyril wrote:

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 wrote:

@CohenCyril note that this actually is a single char change: 48aef72

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).

Sorry for posting in the wrong place. I agree with you and both solutions seem fine as long as one is merged ASAP. I just don't want to pull the rug out from under @pi8027.

Perhaps it's wiser to merge the HB port first though?

[pi8027]

For me, the primary motivation for refactoring multinomials right now is proving an untyping theorem for metrices. I can live with either MC1 or MC2.

[proux01]

Ok, so let's merge #42 first and I'll rebase #80 right after