From e2e23a52655fbd04a1cc659e64fb520d97d7f9db Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 10 Jul 2018 13:04:17 +0200
Subject: Export a function to apply toplevel tactic values in Tacinterp.

This is a function that keeps beeing asked or reimplemented. It doesn't hurt
adding it to the Ltac API.
---
 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 fd2d96bd62..f9883e4441 100644
--- a/plugins/ltac/tacinterp.mli
+++ b/plugins/ltac/tacinterp.mli
@@ -28,6 +28,7 @@ sig
   val to_list : t -> t list option
   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
 end
 
 (** Values for interpretation *)
-- 
cgit v1.2.3