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 <coq-core.plugins.ltac2:plus>
 Call {Control.zero e}
 Prim <coq-core.plugins.ltac2:zero>
-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 <coq-core.plugins.ltac2:plus_bt>
 Call f
 Prim <coq-core.plugins.ltac2:zero>
-Backtrace:
-
 Uncaught Ltac2 exception: Invalid_argument None
 File "./output/ltac2_bt.v", line 11, characters 2-61:
 The command has indeed failed with message: