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

---
 vernac/lemmas.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'vernac')

diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index 1c7cc5e636..2dae0ad125 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -395,10 +395,10 @@ let start_proof_with_initialization ~ontop ?hook kind sigma decl recguard thms s
 	  maybe_declare_manual_implicits false ref imps;
           call_hook ?hook ctx [] strength ref) thms_data in
       let pstate = start_proof ~ontop id ~pl:decl kind sigma t ~hook ~compute_guard:guard in
-      let pstate, _ = Proof_global.with_current_proof (fun _ p ->
+      let pstate = Proof_global.simple_with_current_proof (fun _ p ->
           match init_tac with
-          | None -> p,(true,[])
-          | Some tac -> Proof.run_tactic Global.(env ()) tac p) pstate in
+          | None -> p
+          | Some tac -> pi1 @@ Proof.run_tactic Global.(env ()) tac p) pstate in
       pstate
 
 let start_proof_com ~program_mode ~ontop ?inference_hook ?hook kind thms =
-- 
cgit v1.2.3