From c39b622a8d8b32f335ee7dfe56ad27f9db7caaee Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 9 Apr 2020 23:29:58 +0200
Subject: Export API to recover values out of Ltac application.

---
 plugins/ltac/tacinterp.mli | 1 +
 1 file changed, 1 insertion(+)

(limited to 'plugins/ltac/tacinterp.mli')

diff --git a/plugins/ltac/tacinterp.mli b/plugins/ltac/tacinterp.mli
index ce34356a37..cbb17bf0fa 100644
--- a/plugins/ltac/tacinterp.mli
+++ b/plugins/ltac/tacinterp.mli
@@ -29,6 +29,7 @@ sig
   val of_closure : Geninterp.interp_sign -> glob_tactic_expr -> t
   val cast : 'a typed_abstract_argument_type -> Geninterp.Val.t -> 'a
   val apply : t -> t list -> unit Proofview.tactic
+  val apply_val : t -> t list -> t Ftactic.t
 end
 
 (** Values for interpretation *)
-- 
cgit v1.2.3