From df66f8b8d508c07d218153c313a7877caa9bc1e7 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= Date: Fri, 14 Jun 2024 15:47:25 +0200 Subject: [PATCH] Ltac2 don't print empty backtrace This avoids printing an empty "Backtrace:" entry next to the real one when Ltac2 Backtrace is on. (it gets printed when an exn is wrapped, because the wrapping uses CErrors.print which gives an empty exninfo) It also avoids printing en empty "Backtrace:" for exception which have nothing to do with ltac2 (eg `Check Prop : Prop.`). --- plugins/ltac2/tac2entries.ml | 16 ++++++++-------- test-suite/output/ltac2_bt.out | 4 ---- 2 files changed, 8 insertions(+), 12 deletions(-) diff --git a/plugins/ltac2/tac2entries.ml b/plugins/ltac2/tac2entries.ml index 79ff3e229a52e..700c4ffc6d6e3 100644 --- a/plugins/ltac2/tac2entries.ml +++ b/plugins/ltac2/tac2entries.ml @@ -1019,14 +1019,14 @@ end let () = CErrors.register_additional_error_info begin fun info -> if !Tac2bt.print_ltac2_backtrace then let bt = Exninfo.get info Tac2bt.backtrace in - let bt = match bt with - | Some bt -> List.rev bt - | None -> [] - in - let bt = - str "Backtrace:" ++ fnl () ++ prlist_with_sep fnl pr_frame bt ++ fnl () - in - Some bt + match bt with + | None -> None + | Some bt -> + let bt = List.rev bt in + let bt = + str "Backtrace:" ++ fnl () ++ prlist_with_sep fnl pr_frame bt ++ fnl () + in + Some bt else None end diff --git a/test-suite/output/ltac2_bt.out b/test-suite/output/ltac2_bt.out index eaf77b0f37eb3..3f12f34519114 100644 --- a/test-suite/output/ltac2_bt.out +++ b/test-suite/output/ltac2_bt.out @@ -4,8 +4,6 @@ Backtrace: Prim Call {Control.zero e} Prim -Backtrace: - Uncaught Ltac2 exception: Invalid_argument None File "./output/ltac2_bt.v", line 9, characters 2-49: The command has indeed failed with message: @@ -20,8 +18,6 @@ Backtrace: Prim Call f Prim -Backtrace: - Uncaught Ltac2 exception: Invalid_argument None File "./output/ltac2_bt.v", line 11, characters 2-61: The command has indeed failed with message: