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

---
 tactics/leminv.ml | 5 +----
 1 file changed, 1 insertion(+), 4 deletions(-)

(limited to 'tactics')

diff --git a/tactics/leminv.ml b/tactics/leminv.ml
index 4aa4d13e1e..6efa1ece9c 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.ml
@@ -204,10 +204,7 @@ let inversion_scheme ~name ~poly env sigma t sort dep_option inv_op =
     (str"Computed inversion goal was not closed in initial signature.");
   *)
   let pf = Proof.start ~name ~poly (Evd.from_ctx (evar_universe_context sigma)) [invEnv,invGoal] in
-  let pf =
-    fst (Proof.run_tactic env (
-      tclTHEN intro (onLastHypId inv_op)) pf)
-  in
+  let pf, _, () = Proof.run_tactic env (tclTHEN intro (onLastHypId inv_op)) pf in
   let pfterm = List.hd (Proof.partial_proof pf) in
   let global_named_context = Global.named_context_val () in
   let ownSign = ref begin
-- 
cgit v1.2.3