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

---
 plugins/derive/derive.ml | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

(limited to 'plugins/derive')

diff --git a/plugins/derive/derive.ml b/plugins/derive/derive.ml
index 4425e41652..4769c2dc53 100644
--- a/plugins/derive/derive.ml
+++ b/plugins/derive/derive.ml
@@ -102,6 +102,7 @@ let start_deriving f suchthat lemma =
 
   let terminator = Proof_global.make_terminator terminator in
   let pstate = Proof_global.start_dependent_proof ~ontop:None lemma kind goals terminator in
-  fst @@ Proof_global.with_current_proof begin fun _ p ->
-    Proof.run_tactic env Proofview.(tclFOCUS 1 2 shelve) p
+  Proof_global.simple_with_current_proof begin fun _ p ->
+    let p,_,() =  Proof.run_tactic env Proofview.(tclFOCUS 1 2 shelve) p in
+    p
   end pstate
-- 
cgit v1.2.3