MRE of #416 (comment), which on further inspection seems orthogonal to #416.
There is something weird going on with = instantiations of algebraic datatypes.
theory Thy.
type ATy = [constr].
op useconstr = constr.
end Thy.
clone Thy as Thy1.
clone Thy as Thy2 with
type ATy = Thy1.ATy,
op useconstr <= Thy1.useconstr.
anomaly: File "src/ecUtils.ml", line 239, characters 24-30: Assertion failed
MRE of #416 (comment), which on further inspection seems orthogonal to #416.
There is something weird going on with
=instantiations of algebraic datatypes.