replay: redirect datatype constructors in match bodies too

[MavenRain]

Problem

Cloning a theory while overriding a datatype's type crashes when an operator in that theory
pattern-matches on the datatype's constructors:

theory Thy.
  type ATy = [ CB of int ].
  op getit (x : ATy) = with x = CB n => n.
end Thy.

clone Thy as Thy1.

clone Thy as Thy2 with
  type ATy = Thy1.ATy,
  op getit <= Thy1.getit.

anomaly: EcLib.EcTheoryReplay.CoreIncompatible

Both override modes (type ATy = ... and type ATy <- ...) are affected. Fixes #1046.

Cause

When a datatype's type is overridden, the source datatype's constructors are not re-created in the
clone, so references to them have to be redirected to the target datatype's constructors. #1045
does that with EcSubst.add_opdef, which populates the definition map.

That map is consulted only where a constructor occurs as an operator expression: subst_expr
checks has_opdef at src/ecSubst.ml:335,342 and subst_form at :517,524. A match body
(OP_Fix) does not store its branch constructors as expressions. It stores each one as a bare
path in opb_ctor, which is rewritten through the path map instead
(src/ecSubst.ml:934-935, via subst_path at :74).

So for a match operator the branch constructors were left pointing at the source datatype, and
Compatible.for_opfix, which compares them with EcPath.p_equal
(src/ecTheoryReplay.ml:213), raised CoreIncompatible. Compatible.for_operator catches only
Failure _, so the exception escaped as an anomaly rather than as a clone error.

Fix

Add a dedicated constructor map to EcSubst, sb_ctor, consulted at exactly one place: where a
match branch's opb_ctor path is substituted. replay_tyd records the redirect there alongside
the existing add_opdef entry, in the same fold. On a miss the branch falls through to the
previous subst_path behaviour unchanged, so nothing outside an overridden datatype's match
branches is affected.

A separate map rather than a sb_path entry, because _subst_path recurses into qualifiers
(src/ecSubst.ml:65-72): an entry keyed on Thy.CA would also rewrite every path that Thy.CA
qualifies. Constructor names share a namespace with sub-theories, types and modules, so a sibling
that happens to be named after a constructor would be silently re-rooted into the target datatype's
prefix, changing what replayed definitions denote while their already-proved axioms are re-admitted
unchanged. sb_ctor is keyed exactly and read only for opb_ctor, so it cannot reach any other
position.

Testing

New tests/clone-datatype-match.ec, covering: a match operator overridden through both override
modes; a clone that overrides only the type, with a lemma checking that the replayed match operator
still reduces on the target's constructors; and a recursive match operator, which exercises the
recursive occurrence alongside the constructor redirect.

• Before the change the new test fails with the anomaly, after it passes.
• tests/clone-datatype-alias.ec (the Fix anomaly when alias-cloning a datatype type #1045 / Anomaly caused by algebraic datatype shenanigans #989 regression test) still passes.
• Full unit scenario green: 94/94, including the new test.
• Soundness probes for the namespace-collision case above (a sub-theory, a type, a module and an
  operator named after a constructor of the overridden datatype, plus a rename clause matching a
  constructor name) all behave exactly as on main.

Out of scope, noted for the record

Aliasing the type of a recursive datatype (type RTy = R1.RTy where a constructor takes an
RTy argument) is rejected by the type-compatibility check with

type `RTy` incompatible type declaration

This behaves identically with and without this patch, including when no operator is overridden at
all, so it is pre-existing and independent. The cause looks different in kind: it is the
constructor argument that mentions the datatype itself that is not redirected in alias mode,
whereas inline mode rewrites it through add_tydef. I left it alone rather than widen the scope
here, but I am happy to look at it separately if that is useful.

Relatedly, Compatible.for_operator has no CoreIncompatible handler, unlike for_tydecl
(src/ecTheoryReplay.ml:208). That is why this bug presented as an anomaly instead of a clone
error, and any other operator-body mismatch reaching check would do the same. Adding
| CoreIncompatible -> raise (Incompatible OpBody) would route it through CE_OpIncompatible. I
have not included it here since it changes unrelated error paths, but say the word and I will add
it to this PR or a follow-up.

_{Drafted with AI assistance; the diagnosis, the code, and every claim above were reviewed and
tested by me against a local build.}