From d3a6453f1447bfb956547050ddbd005f4b4751b6 Mon Sep 17 00:00:00 2001
From: Arnaud Spiwack
Date: Mon, 9 Dec 2013 11:15:22 +0100
Subject: 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]).---
 tactics/tacinterp.ml | 5 ++---
 1 file 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
-- 
cgit v1.2.3