Switch axiom replay to use exact rather than a custom apply variant

[oskgo]

Fixes #1006 (comment), but not the other issues, which are orthogonal.

The custom apply variant was introduced by #312. I don't understand why that was done. It seems unrelated to the example in #292.

[Copilot]

Pull request overview

This PR updates theory cloning’s axiom replay mechanism to use the standard apply … exact path (rather than a custom ExactType apply variant), addressing the reported anomaly during reduction/typing in the presence of parametric axioms/subtypes.

Changes:

• Switch axiom override replay in ecThCloning to generate an apply … exact tactic instead of the custom ExactType apply mode.
• Remove the ExactType constructor from the parsetree and delete the corresponding processing code in ecHiGoal.
• Add a regression test covering cloning an axiom with a more polymorphic lemma (tests/clone-parametric-axiom.ec).

Reviewed changes

Copilot reviewed 4 out of 4 changed files in this pull request and generated 1 comment.

File	Description
tests/clone-parametric-axiom.ec	Adds a regression test for cloning a parametric axiom overridden by a polymorphic lemma.
src/ecThCloning.ml	Changes axiom replay tactic generation to use apply with Exact mode.
src/ecParsetree.ml	Removes the ExactType apply variant from the AST.
src/ecHiGoal.ml	Removes the implementation handling the deleted ExactType variant.

---

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.