Adding a way to inject tactic closures in interpretation values.

2 files changed, 26 insertions, 17 deletions

diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 5e44652132..0077f05686 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -61,7 +61,31 @@ let (wit_tacvalue : (Empty.t, Empty.t, tacvalue) Genarg.genarg_type) =
 let of_tacvalue v = in_gen (topwit wit_tacvalue) v
 let to_tacvalue v = out_gen (topwit wit_tacvalue) v
 
-module Value = Taccoerce.Value
+module TacStore = Geninterp.TacStore
+
+let f_avoid_ids : Id.t list TacStore.field = TacStore.field ()
+(* ids inherited from the call context (needed to get fresh ids) *)
+let f_debug : debug_info TacStore.field = TacStore.field ()
+let f_trace : ltac_trace TacStore.field = TacStore.field ()
+
+(* Signature for interpretation: val_interp and interpretation functions *)
+type interp_sign = Geninterp.interp_sign = {
+  lfun : value Id.Map.t;
+  extra : TacStore.t }
+
+let extract_trace ist = match TacStore.get ist.extra f_trace with
+| None -> []
+| Some l -> l
+
+module Value = struct
+
+  include Taccoerce.Value
+
+  let of_closure ist tac =
+    let closure = VFun (extract_trace ist, ist.lfun, [], tac) in
+    of_tacvalue closure
+
+end
 
 let dloc = Loc.ghost
 
@@ -77,13 +101,6 @@ let catching_error call_trace fail e =
     fail located_exc
   end
 
-module TacStore = Geninterp.TacStore
-
-let f_avoid_ids : Id.t list TacStore.field = TacStore.field ()
-(* ids inherited from the call context (needed to get fresh ids) *)
-let f_debug : debug_info TacStore.field = TacStore.field ()
-let f_trace : ltac_trace TacStore.field = TacStore.field ()
-
 let catch_error call_trace f x =
   try f x
   with e when Errors.noncritical e ->
@@ -95,11 +112,6 @@ let catch_error_tac call_trace tac =
     tac
     (catching_error call_trace Proofview.tclZERO)
 
-(* Signature for interpretation: val_interp and interpretation functions *)
-type interp_sign = Geninterp.interp_sign = {
-  lfun : value Id.Map.t;
-  extra : TacStore.t }
-
 let curr_debug ist = match TacStore.get ist.extra f_debug with
 | None -> DebugOff
 | Some level -> level
@@ -175,10 +187,6 @@ let push_trace call ist = match TacStore.get ist.extra f_trace with
 | None -> [call]
 | Some trace -> call :: trace
 
-let extract_trace ist = match TacStore.get ist.extra f_trace with
-| None -> []
-| Some l -> l
-
 let propagate_trace ist loc id v =
   let v = Value.normalize v in
   if has_type v (topwit wit_tacvalue) then
diff --git a/tactics/tacinterp.mli b/tactics/tacinterp.mli
index 78db212121..72d545d6c7 100644
--- a/tactics/tacinterp.mli
+++ b/tactics/tacinterp.mli
@@ -22,6 +22,7 @@ sig
   val of_int : int -> t
   val to_int : t -> int option
   val to_list : t -> t list option
+  val of_closure : Geninterp.interp_sign -> glob_tactic_expr -> t
 end
 
 (** Values for interpretation *)