From 982c1ae49d200f782a5b82f53164d68418a77387 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 6 Sep 2013 22:01:36 +0200
Subject: Adding the necessary hooks to handle tactics in terms.

---
 interp/genintern.ml  |  2 ++
 tactics/tacinterp.ml | 19 +++++++++++++++++++
 2 files changed, 21 insertions(+)

diff --git a/interp/genintern.ml b/interp/genintern.ml
index 86a1ce1f5d..d1bc28333b 100644
--- a/interp/genintern.ml
+++ b/interp/genintern.ml
@@ -54,3 +54,5 @@ let register_subst0 = Subst.register0
 let generic_substitute subs v =
   let unpack wit v = in_gen (glbwit wit) (substitute wit subs v) in
   glb_unpack { glb_unpack = unpack; } v
+
+let () = Hook.set Detyping.subst_genarg_hook generic_substitute
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 845b3ad9fb..0821423b5d 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -2188,6 +2188,25 @@ let tacticIn t =
 (***************************************************************************)
 (* Backwarding recursive needs of tactic glob/interp/eval functions *)
 
+let _ =
+  let eval ty env sigma lfun arg =
+    let ist = { lfun = lfun; extra = TacStore.empty; } in
+    if has_type arg (glbwit wit_tactic) then
+      let tac = out_gen (glbwit wit_tactic) arg in
+      let tac = interp_tactic ist tac in
+      let prf = Proof.start sigma [env, ty] in
+      let (prf, _) = Proof.run_tactic env tac prf in
+      let sigma = Proof.in_proof prf (fun sigma -> sigma) in
+      let ans = match Proof.initial_goals prf with
+      | [c, _] -> c
+      | _ -> assert false
+      in
+      ans, sigma
+    else
+      failwith "not a tactic"
+  in
+  Hook.set Pretyping.genarg_interp_hook eval
+
 let _ = Hook.set Auto.extern_interp
   (fun l ->
     let lfun = Id.Map.map (fun c -> Value.of_constr c) l in
-- 
cgit v1.2.3