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

Author: oskgo

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

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
 ]
 
 (* -------------------------------------------------------------------- *)

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

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.