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

---
 stm/stm.ml | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

(limited to 'stm')

diff --git a/stm/stm.ml b/stm/stm.ml
index 3eb6d03529..21618bc044 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -2085,8 +2085,8 @@ end = struct (* {{{ *)
     let st = Vernacstate.freeze_interp_state ~marshallable:false in
     stm_fail ~st fail (fun () ->
     (if time then System.with_time ~batch ~header:(Pp.mt ()) else (fun x -> x)) (fun () ->
-    ignore(TaskQueue.with_n_workers nworkers (fun queue ->
-    PG_compat.with_current_proof (fun _ p ->
+    TaskQueue.with_n_workers nworkers (fun queue ->
+    PG_compat.simple_with_current_proof (fun _ p ->
       let Proof.{goals} = Proof.data p in
       let open TacTask in
       let res = CList.map_i (fun i g ->
@@ -2131,7 +2131,8 @@ end = struct (* {{{ *)
             if solve then Tacticals.New.tclSOLVE [] else tclUNIT ()
         end)
       in
-      Proof.run_tactic (Global.env()) assign_tac p)))) ())
+      let p,_,() = Proof.run_tactic (Global.env()) assign_tac p in
+      p))) ())
 
 end (* }}} *)
 
-- 
cgit v1.2.3