From 682ec8fe694e37757d2cd6c98fb5e2e609a6f08f Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Thu, 9 May 2019 14:07:16 +0200
Subject: Allow run_tactic to return a value, remove hack from ltac2

---
 proofs/proof.mli | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'proofs/proof.mli')

diff --git a/proofs/proof.mli b/proofs/proof.mli
index 1f4748141a..248b9d921e 100644
--- a/proofs/proof.mli
+++ b/proofs/proof.mli
@@ -172,7 +172,7 @@ val no_focused_goal : t -> bool
    used. In which case it is [false]. *)
 val run_tactic
   :  Environ.env
-  -> unit Proofview.tactic -> t -> t * (bool*Proofview_monad.Info.tree)
+  -> 'a Proofview.tactic -> t -> t * (bool*Proofview_monad.Info.tree) * 'a
 
 val maximal_unfocus : 'a focus_kind -> t -> t
 
-- 
cgit v1.2.3