From a059c181c3b2d6c1f9c3682c15270c0942430f39 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sat, 9 Sep 2017 20:40:11 +0200
Subject: Fix coq/ltac2#18: Terms should show a backtrace when Set Ltac2
 Backtrace is set.

---
 src/tac2core.ml | 1 +
 1 file changed, 1 insertion(+)

(limited to 'src')

diff --git a/src/tac2core.ml b/src/tac2core.ml
index ab87fa7739..9920b4c805 100644
--- a/src/tac2core.ml
+++ b/src/tac2core.ml
@@ -799,6 +799,7 @@ let interp_constr flags ist c =
     Proofview.tclUNIT c
   with e when catchable_exception e ->
     let (e, info) = CErrors.push e in
+    set_bt info >>= fun info ->
     match Exninfo.get info fatal_flag with
     | None -> Proofview.tclZERO ~info e
     | Some () -> throw ~info e
-- 
cgit v1.2.3