Running
theory T.
op x = 4.
end T.
clone T as T' with
op x <- 3.
gives the error
anomaly: EcLib.EcTheoryReplay.CoreIncompatible
Because errors about rewriting in clones are all localized at the
keyword clone, as opposed to the offending rewriting, this anomaly
needs to be turned into an error message that says (by analogy with
the error for type rewriting):
operator `x` incompatible operator declaration
or better
incompatible rewriting for operator `x`