From 3007909ca1f65132bd0850d2be57e781e55707bd Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 2 Aug 2017 18:51:19 +0200
Subject: Tentatively implementing apply.

---
 src/tac2stdlib.ml | 12 ++++++++++++
 1 file changed, 12 insertions(+)

(limited to 'src/tac2stdlib.ml')

diff --git a/src/tac2stdlib.ml b/src/tac2stdlib.ml
index f63252ec22..b678b65b82 100644
--- a/src/tac2stdlib.ml
+++ b/src/tac2stdlib.ml
@@ -12,6 +12,7 @@ open Misctypes
 open Genredexpr
 open Tac2expr
 open Tac2core
+open Tac2tactics
 open Proofview.Notations
 
 module Value = Tac2ffi
@@ -178,6 +179,17 @@ let () = define_prim2 "tac_intros" begin fun ev ipat ->
   Tactics.intros_patterns ev ipat
 end
 
+let () = define_prim4 "tac_apply" begin fun adv ev cb ipat ->
+  let adv = Value.to_bool adv in
+  let ev = Value.to_bool ev in
+  let map_cb c = thaw c >>= fun c -> return (to_constr_with_bindings c) in
+  let cb = Value.to_list map_cb cb in
+  let map p = Value.to_option (fun p -> Loc.tag (to_intro_pattern p)) p in
+  let map_ipat p = to_pair Value.to_ident map p in
+  let ipat = Value.to_option map_ipat ipat in
+  Tac2tactics.apply adv ev cb ipat
+end
+
 let () = define_prim3 "tac_elim" begin fun ev c copt ->
   let ev = Value.to_bool ev in
   let c = to_constr_with_bindings c in
-- 
cgit v1.2.3