diff options
| author | Pierre-Marie Pédrot | 2017-10-01 19:10:11 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-10-01 19:18:59 +0200 |
| commit | 0145084daa86b35a1d2a8285c4e16a9a231e3652 (patch) | |
| tree | 5a589caf12c346ec9a1ac17521d35a07191eddd5 /src/tac2tactics.ml | |
| parent | 95f0ba81363a464e416fa2fdba3e4170accd4d96 (diff) | |
Using Ltac2 native closures in some tactic APIs.
Diffstat (limited to 'src/tac2tactics.ml')
| -rw-r--r-- | src/tac2tactics.ml | 7 |
1 files changed, 6 insertions, 1 deletions
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 = |