Fix anomaly when alias-cloning a datatype type

[strub]

Closes #989.

Problem

Overriding a datatype's type with another datatype via a plain alias (type ATy = ...) crashed during cloning:

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 ... Assertion failed (an oget None).

Cause

When a datatype's type is overridden during cloning, the source datatype's constructors are not re-created in the clone (the new type isn't a Datatype). References to those constructors — e.g. in operator bodies — must therefore be redirected to the target datatype's constructors.

EcTheoryReplay.replay_tyd did exactly that, but only inside the Inline _ branch (<- / <=). For a plain alias override (= → Alias), the source constructor paths were instead renamed to non-existent paths (Thy2.constr); force-reducing them in the operator-compatibility check tripped the oget None.

Fix

Lift the constructor-remapping out of the inline-only branch so it runs after the mode match, for every override mode. The substitution in scope at that point is already correct for both modes (rename for alias, add_tydef for inline).

Regression test added: tests/clone-datatype-alias.ec.

Notes / out of scope

This is a surgical fix; it will be subsumed by the planned refactor that introduces an explicit elaborator for derived objects (constructors, projectors, _ind/_case). Two related issues are left untouched as pre-existing and orthogonal (they reproduce on main, in both override modes):

• Operator bodies that match on constructors (OP_Fix) still fail with CoreIncompatible under a datatype-type override — the remap only covers OP_Constr, not match bodies.
• Polymorphic op overrides (op mk <= Thy1.mk with a type variable) fail with "operator body contains 0 type parameter instead of 1".