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.

---
 theories/Control.v | 7 +++++++
 1 file changed, 7 insertions(+)

(limited to 'theories/Control.v')

diff --git a/theories/Control.v b/theories/Control.v
index a6d46a89a8..a8b92aced2 100644
--- a/theories/Control.v
+++ b/theories/Control.v
@@ -54,3 +54,10 @@ Ltac2 @ external hyps : unit -> (ident * constr option * constr) list := "ltac2"
 (** Refinement *)
 
 Ltac2 @ external refine : (unit -> constr) -> unit := "ltac2" "refine".
+
+(** Evars *)
+
+Ltac2 @ external with_holes : (unit -> 'a) -> ('a -> 'b) -> 'b := "ltac2" "with_holes".
+(** [with_holes x f] evaluates [x], then apply [f] to the result, and fails if
+    all evars generated by the call to [x] have not been solved when [f]
+    returns. *)
-- 
cgit v1.2.3