https://github.com/math-comp/math-comp/pull/1256 generalizes operations. This PR generalizes everything that was on nmodType to baseAddUMagmaType (and addition to addMagmaType). It also changes the mem predicate in common.elpi to use coq.unify-eq because elpi's unification is not module delta, which causes issues when N-modules are cast to baseAddUMagmaType.
https://github.com/math-comp/math-comp/pull/1256 generalizes operations. This PR generalizes everything that was on
nmodTypetobaseAddUMagmaType(and addition toaddMagmaType). It also changes themempredicate incommon.elpito usecoq.unify-eqbecauseelpi's unification is not module delta, which causes issues when N-modules are cast tobaseAddUMagmaType.