From 9262f440e8d8b8559c5488b1333c023f7305d811 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>
Date: Wed, 30 Nov 2016 23:08:19 +0100
Subject: Allowing to pass arbitrary data in internalization environments.

---
 plugins/ltac/tacinterp.ml | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

(limited to 'plugins/ltac/tacinterp.ml')

diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index b8c021f18..5f831f326 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -587,6 +587,7 @@ let interp_uconstr ist env sigma = function
       let ltacvars = {
         Constrintern.ltac_vars = Id.(Set.union (Map.domain typed) (Map.domain untyped));
         ltac_bound = Id.Map.domain ist.lfun;
+        ltac_extra = Genintern.Store.empty;
       } in
       { closure ; term =  intern_gen WithoutTypeConstraint ~ltacvars env ce }
 
@@ -614,6 +615,7 @@ let interp_gen kind ist allow_patvar flags env sigma (c,ce) =
       let ltacvars = {
         ltac_vars = constr_context;
         ltac_bound = Id.Map.domain ist.lfun;
+        ltac_extra = Genintern.Store.empty;
       } in
       let kind_for_intern =
         match kind with OfType _ -> WithoutTypeConstraint | _ -> kind in
@@ -1966,8 +1968,7 @@ let interp_tac_gen lfun avoid_ids debug t =
   let ist = { lfun = lfun; extra = extra } in
   let ltacvars = Id.Map.domain lfun in
   interp_tactic ist
-    (intern_pure_tactic {
-      ltacvars; genv = env } t)
+    (intern_pure_tactic { (Genintern.empty_glob_sign env) with ltacvars } t)
   end }
 
 let interp t = interp_tac_gen Id.Map.empty [] (get_debug()) t
@@ -1976,7 +1977,7 @@ let interp t = interp_tac_gen Id.Map.empty [] (get_debug()) t
 (* [global] means that [t] should be internalized outside of goals. *)
 let hide_interp global t ot =
   let hide_interp env =
-    let ist = { ltacvars = Id.Set.empty; genv = env } in
+    let ist = Genintern.empty_glob_sign env in
     let te = intern_pure_tactic ist t in
     let t = eval_tactic te in
     match ot with
-- 
cgit v1.2.3


From 173f32406be06ad4dfcecf3cda6070543d68d715 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>
Date: Wed, 7 Dec 2016 14:07:28 +0100
Subject: Generalizing the tactic-in-term embedding to any generic argument.

---
 plugins/ltac/tacinterp.ml | 14 +++++---------
 pretyping/pretyping.ml    | 17 +++++++++++++++--
 pretyping/pretyping.mli   |  6 +++---
 3 files changed, 23 insertions(+), 14 deletions(-)

(limited to 'plugins/ltac/tacinterp.ml')

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
-- 
cgit v1.2.3