Using Ltac2 native closures in some tactic APIs.

5 files changed, 14 insertions, 5 deletions

diff --git a/src/tac2ffi.ml b/src/tac2ffi.ml
index 7960d4d45f..923a29e5c5 100644
--- a/src/tac2ffi.ml
+++ b/src/tac2ffi.ml
@@ -329,6 +329,7 @@ let reference = {
 type ('a, 'b) fun1 = closure
 
 let fun1 (r0 : 'a repr) (r1 : 'b repr) : ('a, 'b) fun1 repr = closure
+let to_fun1 r0 r1 f = to_closure f
 
 let rec apply : type a. a arity -> a -> valexpr list -> valexpr Proofview.tactic =
   fun arity f args -> match args, arity with
diff --git a/src/tac2ffi.mli b/src/tac2ffi.mli
index 36743f3346..cb6d5a1e49 100644
--- a/src/tac2ffi.mli
+++ b/src/tac2ffi.mli
@@ -143,6 +143,7 @@ type ('a, 'b) fun1
 
 val app_fun1 : ('a, 'b) fun1 -> 'a repr -> 'b repr -> 'a -> 'b Proofview.tactic
 
+val to_fun1 : 'a repr -> 'b repr -> valexpr -> ('a, 'b) fun1
 val fun1 : 'a repr -> 'b repr -> ('a, 'b) fun1 repr
 
 val valexpr : valexpr repr
diff --git a/src/tac2stdlib.ml b/src/tac2stdlib.ml
index 4bcbe69b07..2828bbc53f 100644
--- a/src/tac2stdlib.ml
+++ b/src/tac2stdlib.ml
@@ -108,7 +108,7 @@ and to_intro_pattern_action = function
   let map ipat = to_intro_pattern ipat in
   IntroInjection (Value.to_list map inj)
 | ValBlk (2, [| c; ipat |]) ->
-  let c = thaw c >>= fun c -> return (Value.to_constr c) in
+  let c = Value.to_fun1 Value.unit Value.constr c in
   IntroApplyOn (c, to_intro_pattern ipat)
 | ValBlk (3, [| b |]) -> IntroRewrite (Value.to_bool b)
 | _ -> assert false
@@ -143,7 +143,7 @@ let to_induction_clause v = match Value.to_tuple v with
 
 let to_assertion v = match Value.to_block v with
 | (0, [| ipat; t; tac |]) ->
-  let to_tac t = Proofview.tclIGNORE (thaw t) in
+  let to_tac t = Value.to_fun1 Value.unit Value.unit t in
   let ipat = Value.to_option to_intro_pattern ipat in
   let t = Value.to_constr t in
   let tac = Value.to_option to_tac tac in
diff --git a/src/tac2tactics.ml b/src/tac2tactics.ml
index b55bd5c1b8..0b25ebb378 100644
--- a/src/tac2tactics.ml
+++ b/src/tac2tactics.ml
@@ -17,6 +17,7 @@ open Proofview
 open Proofview.Notations
 
 let return = Proofview.tclUNIT
+let thaw r f = Tac2ffi.app_fun1 f Tac2ffi.unit r ()
 
 let tactic_infer_flags with_evar = {
   Pretyping.use_typeclasses = true;
@@ -31,6 +32,9 @@ let delayed_of_tactic tac env sigma =
   let c, pv, _, _ = Proofview.apply env tac pv in
   (sigma, c)
 
+let delayed_of_thunk r tac env sigma =
+  delayed_of_tactic (thaw r tac) env sigma
+
 let mk_bindings = function
 | ImplicitBindings l -> Misctypes.ImplicitBindings l
 | ExplicitBindings l ->
@@ -55,7 +59,7 @@ and mk_intro_pattern_action = function
 | IntroOrAndPattern ipat -> Misctypes.IntroOrAndPattern (mk_or_and_intro_pattern ipat)
 | IntroInjection ipats -> Misctypes.IntroInjection (List.map mk_intro_pattern ipats)
 | IntroApplyOn (c, ipat) ->
-  let c = Loc.tag @@ delayed_of_tactic c in
+  let c = Loc.tag @@ delayed_of_thunk Tac2ffi.constr c in
   Misctypes.IntroApplyOn (c, mk_intro_pattern ipat)
 | IntroRewrite b -> Misctypes.IntroRewrite b
 
@@ -172,6 +176,7 @@ let assert_ = function
   Tactics.forward true None (Some ipat) c
 | AssertType (ipat, c, tac) ->
   let ipat = Option.map mk_intro_pattern ipat in
+  let tac = Option.map (fun tac -> thaw Tac2ffi.unit tac) tac in
   Tactics.forward true (Some tac) ipat c
 
 let letin_pat_tac ev ipat na c cl =
diff --git a/src/tac2types.mli b/src/tac2types.mli
index 1cacbefc88..a7b0ceed6e 100644
--- a/src/tac2types.mli
+++ b/src/tac2types.mli
@@ -15,6 +15,8 @@ open Proofview
 type evars_flag = bool
 type advanced_flag = bool
 
+type 'a thunk = (unit, 'a) Tac2ffi.fun1
+
 type quantified_hypothesis = Misctypes.quantified_hypothesis =
 | AnonHyp of int
 | NamedHyp of Id.t
@@ -47,7 +49,7 @@ and intro_pattern_action =
 | IntroWildcard
 | IntroOrAndPattern of or_and_intro_pattern
 | IntroInjection of intro_pattern list
-| IntroApplyOn of EConstr.t tactic * intro_pattern
+| IntroApplyOn of EConstr.t thunk * intro_pattern
 | IntroRewrite of bool
 and or_and_intro_pattern =
 | IntroOrPattern of intro_pattern list list
@@ -86,5 +88,5 @@ type rewriting =
   constr_with_bindings tactic
 
 type assertion =
-| AssertType of intro_pattern option * constr * unit tactic option
+| AssertType of intro_pattern option * constr * unit thunk option
 | AssertValue of Id.t * constr