Generalizing the tactic-in-term embedding to any generic argument.

3 files changed, 23 insertions, 14 deletions

diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index 5f831f326..7f7a64338 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -2100,17 +2100,13 @@ let interp_redexp env sigma r =
 (* Backwarding recursive needs of tactic glob/interp/eval functions *)
 
 let _ =
-  let eval ty env sigma lfun arg =
+  let eval lfun env sigma ty tac =
     let ist = { lfun = lfun; extra = TacStore.empty; } in
-    if Genarg.has_type arg (glbwit wit_tactic) then
-      let tac = Genarg.out_gen (glbwit wit_tactic) arg in
-      let tac = interp_tactic ist tac in
-      let (c, sigma) = Pfedit.refine_by_tactic env sigma ty tac in
-      (EConstr.of_constr c, sigma)
-    else
-      failwith "not a tactic"
+    let tac = interp_tactic ist tac in
+    let (c, sigma) = Pfedit.refine_by_tactic env sigma ty tac in
+    (EConstr.of_constr c, sigma)
   in
-  Hook.set Pretyping.genarg_interp_hook eval
+  Pretyping.register_constr_interp0 wit_tactic eval
 
 (** Used in tactic extension **)
 
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 68ef97659..fa37f8cf6 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -560,7 +560,17 @@ let new_type_evar env evdref loc =
   evdref := Sigma.to_evar_map sigma;
   e
 
-let (f_genarg_interp, genarg_interp_hook) = Hook.make ()
+module ConstrInterpObj =
+struct
+  type ('r, 'g, 't) obj =
+    unbound_ltac_var_map -> env -> evar_map -> types -> 'g -> constr * evar_map
+  let name = "constr_interp"
+  let default _ = None
+end
+
+module ConstrInterp = Genarg.Register(ConstrInterpObj)
+
+let register_constr_interp0 = ConstrInterp.register0
 
 (* [pretype tycon env evdref lvar lmeta cstr] attempts to type [cstr] *)
 (* in environment [env], with existential variables [evdref] and *)
@@ -620,8 +630,11 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
         | Some ty -> ty
         | None ->
           new_type_evar env evdref loc in
+      let open Genarg in
       let ist = lvar.ltac_genargs in
-      let (c, sigma) = Hook.get f_genarg_interp ty env.ExtraEnv.env !evdref ist arg in
+      let GenArg (Glbwit tag, arg) = arg in
+      let interp = ConstrInterp.obj tag in
+      let (c, sigma) = interp ist env.ExtraEnv.env !evdref ty arg in
       let () = evdref := sigma in
       { uj_val = c; uj_type = ty }
 
diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli
index f13c10b05..41f0a5fad 100644
--- a/pretyping/pretyping.mli
+++ b/pretyping/pretyping.mli
@@ -163,6 +163,6 @@ val ise_pretype_gen :
 val interp_sort : ?loc:Loc.t -> evar_map -> glob_sort -> evar_map * sorts
 val interp_elimination_sort : glob_sort -> sorts_family
 
-val genarg_interp_hook :
-  (types -> env -> evar_map -> unbound_ltac_var_map ->
-    Genarg.glob_generic_argument -> constr * evar_map) Hook.t
+val register_constr_interp0 :
+  ('r, 'g, 't) Genarg.genarg_type ->
+    (unbound_ltac_var_map -> env -> evar_map -> types -> 'g -> constr * evar_map) -> unit