From 08f8791299456984b753938b46e9d5545c9be998 Mon Sep 17 00:00:00 2001
From: Oskar Goldhahn <oskar.goldhahn@ntnu.no>
Date: Wed, 3 Jun 2026 17:15:47 +0200
Subject: [PATCH] switch axiom replay to use `exact` rather than a custom apply
 variant

---
 src/ecHiGoal.ml                 | 22 ----------------------
 src/ecParsetree.ml              |  1 -
 src/ecThCloning.ml              |  4 +++-
 tests/clone-parametric-axiom.ec | 10 ++++++++++
 4 files changed, 13 insertions(+), 24 deletions(-)
 create mode 100644 tests/clone-parametric-axiom.ec

diff --git a/src/ecHiGoal.ml b/src/ecHiGoal.ml
index 5505e655f..1d22fd9c0 100644
--- a/src/ecHiGoal.ml
+++ b/src/ecHiGoal.ml
@@ -562,25 +562,6 @@ let process_apply_bwd ~implicits mode (ff : ppterm) (tc : tcenv1) =
   with (EcLowGoal.Apply.NoInstance _) as err ->
     tc_error_exn !!tc err
 
-(* -------------------------------------------------------------------- *)
-let process_exacttype qs (tc : tcenv1) =
-  let env, hyps, _ = FApi.tc1_eflat tc in
-  let p =
-    try EcEnv.Ax.lookup_path (EcLocation.unloc qs) env
-    with LookupFailure cause ->
-      tc_error !!tc "%a" EcEnv.pp_lookup_failure cause
-  in
-  let tys =
-    List.map (fun a -> EcTypes.tvar a)
-      (EcEnv.LDecl.tohyps hyps).h_tvar in
-  let pt = ptglobal ~tys p in
-
-  try
-    EcLowGoal.t_apply pt tc
-  with InvalidGoalShape ->
-    let ppe = EcPrinting.PPEnv.ofenv env in
-    tc_error !!tc "cannot apply %a@." (EcPrinting.pp_axname ppe) p
-
 (* -------------------------------------------------------------------- *)
 let process_apply_fwd ~implicits (pe, hyp) tc =
   let module E = struct exception NoInstance end in
@@ -2048,9 +2029,6 @@ let process_apply ~implicits ((infos, orv) : apply_t * prevert option) tc =
     | `Alpha pe ->
         process_apply_bwd ~implicits `Alpha pe tc
 
-    | `ExactType qs ->
-        process_exacttype qs tc
-
     | `Top mode ->
         let tc = process_apply_top tc in
         if mode = `Exact then t_onall process_done tc else tc
diff --git a/src/ecParsetree.ml b/src/ecParsetree.ml
index 8c2ccbadc..e9deac3f9 100644
--- a/src/ecParsetree.ml
+++ b/src/ecParsetree.ml
@@ -1034,7 +1034,6 @@ type apply_info = [
   | `Apply   of ppterm list * [`Apply|`Exact|`Alpha]
   | `Top     of [`Apply|`Exact|`Alpha]
   | `Alpha   of ppterm
-  | `ExactType of pqsymbol
 ]
 
 (* -------------------------------------------------------------------- *)
diff --git a/src/ecThCloning.ml b/src/ecThCloning.ml
index e55075da2..121a10858 100644
--- a/src/ecThCloning.ml
+++ b/src/ecThCloning.ml
@@ -391,7 +391,9 @@ end = struct
   (* ------------------------------------------------------------------ *)
   let ax_ovrd _oc ((proofs, evc) : state) name ((axd, mode) : ax_override) =
     let loc = axd.pl_loc in
-    let tc = Papply (`ExactType axd, None) in
+    let tc = FPNamed (axd, None) in
+    let tc = { fp_mode = `Explicit; fp_head = tc; fp_args = []; } in
+    let tc = Papply (`Apply ([tc], `Exact), None) in
     let tc = mk_loc loc (Plogic tc) in
     let pr = { pthp_mode   = `Named (name, mode);
                pthp_tactic = Some tc; } in
diff --git a/tests/clone-parametric-axiom.ec b/tests/clone-parametric-axiom.ec
new file mode 100644
index 000000000..7a1d76190
--- /dev/null
+++ b/tests/clone-parametric-axiom.ec
@@ -0,0 +1,10 @@
+op gen ['a]: bool = true.
+
+theory T.
+axiom ax : gen<:bool>.
+end T.
+
+lemma lem: gen<:'a> by done.
+
+clone T as T' with
+axiom ax <- lem.
\ No newline at end of file