From 91a9313fbe24dfb0c9b7fcaa31e3c11bf055450a Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sat, 9 Sep 2017 20:43:32 +0200
Subject: Fix coq/ltac2#26: Ltac1 gives no backtraces.

---
 src/tac2core.ml | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

(limited to 'src')

diff --git a/src/tac2core.ml b/src/tac2core.ml
index 9920b4c805..f19f45fa4e 100644
--- a/src/tac2core.ml
+++ b/src/tac2core.ml
@@ -895,7 +895,9 @@ let () =
     let ist = Ltac_plugin.Tacinterp.default_ist () in
     (** FUCK YOU API *)
     let ist = { ist with API.Geninterp.lfun = (Obj.magic lfun) } in
-    (Obj.magic Ltac_plugin.Tacinterp.eval_tactic_ist ist tac : unit Proofview.tactic) >>= fun () ->
+    let tac = (Obj.magic Ltac_plugin.Tacinterp.eval_tactic_ist ist tac : unit Proofview.tactic) in
+    let wrap (e, info) = set_bt info >>= fun info -> Proofview.tclZERO ~info e in
+    Proofview.tclOR tac wrap >>= fun () ->
     return v_unit
   in
   let subst s tac = Genintern.substitute Ltac_plugin.Tacarg.wit_tactic s tac in
-- 
cgit v1.2.3