algebra-tactics icon indicating copy to clipboard operation
algebra-tactics copied to clipboard
verified publisher icon math-comp

adapt to MC#1256

Open Tragicus opened this issue 1 year ago • 0 comments

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.

Tragicus avatar Aug 21 '24 15:08 Tragicus