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

@@ -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
 

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: