From c7c1f9b2da838a604c479bb2bc162fef621524ed Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sat, 9 Sep 2017 20:46:59 +0200
Subject: If backtrace is missing, don't print it.

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

(limited to 'src')

diff --git a/src/tac2entries.ml b/src/tac2entries.ml
index 208231b814..26f96f7d72 100644
--- a/src/tac2entries.ml
+++ b/src/tac2entries.ml
@@ -782,7 +782,10 @@ end
 let () = ExplainErr.register_additional_error_info begin fun (e, info) ->
   if !Tac2interp.print_ltac2_backtrace then
     let bt = Exninfo.get info backtrace in
-    let bt = Option.default [] bt in
+    let bt = match bt with
+    | Some bt -> bt
+    | None -> raise Exit
+    in
     let bt =
       str "Backtrace:" ++ fnl () ++ prlist_with_sep fnl pr_frame bt ++ fnl ()
     in
-- 
cgit v1.2.3