Stylistic change.

I doubt [catching_error] is performance critical in any way. But it looked silly to allocate a block to [(inner_trace,e)] when [e] was known in advance (and was already named [e]).

1 files changed, 2 insertions, 3 deletions

diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 59c8992c51..b86326dda3 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -70,9 +70,8 @@ let dloc = Loc.ghost
 
 let catching_error call_trace fail e =
   let e = Errors.push e in
-  let inner_trace, e = match Exninfo.get e ltac_trace_info with
-  | Some inner_trace -> inner_trace, e
-  | None -> [], e
+  let inner_trace =
+    Option.default [] (Exninfo.get e ltac_trace_info)
   in
   if List.is_empty call_trace && List.is_empty inner_trace then fail e
   else begin