Skip to content

remove an unnecessary premise from big_opM_own_1

Ralf Jung requested to merge ralf/big_opM_own_1 into master

The way big_opM_own_1 was stated, it requires an element of type B, which is totally unnecessary.

Merge request reports