From 0f72b089de52ad7d26d71e56003b140fa5012635 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 28 Jul 2017 17:53:42 +0200
Subject: Exporting more internals from Coq implementation.

---
 src/tac2core.ml | 9 +++++++++
 1 file changed, 9 insertions(+)

(limited to 'src/tac2core.ml')

diff --git a/src/tac2core.ml b/src/tac2core.ml
index f28c5c5dcf..515cadc525 100644
--- a/src/tac2core.ml
+++ b/src/tac2core.ml
@@ -557,6 +557,14 @@ let prm_refine : ml_tactic = function
   end >>= fun () -> return v_unit
 | _ -> assert false
 
+let prm_with_holes : ml_tactic = function
+| [x; f] ->
+  Proofview.tclEVARMAP >>= fun sigma0 ->
+  thaw x >>= fun ans ->
+  Proofview.tclEVARMAP >>= fun sigma ->
+  Proofview.Unsafe.tclEVARS sigma0 >>= fun () ->
+  Tacticals.New.tclWITHHOLES false (interp_app f [ans]) sigma
+| _ -> assert false
 
 (** Registering *)
 
@@ -615,6 +623,7 @@ let () = Tac2env.define_primitive (pname "goal") prm_goal
 let () = Tac2env.define_primitive (pname "hyp") prm_hyp
 let () = Tac2env.define_primitive (pname "hyps") prm_hyps
 let () = Tac2env.define_primitive (pname "refine") prm_refine
+let () = Tac2env.define_primitive (pname "with_holes") prm_with_holes
 
 (** ML types *)
 
-- 
cgit v1.2.3