Removing a useless location in ltac trace mechanism.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16547 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 4 insertions, 9 deletions

diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 6c66f4ced..761dfe6a9 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -71,20 +71,15 @@ let dloc = Loc.ghost
 let catch_error call_trace tac g =
   try tac g with e when Errors.noncritical e ->
   let e = Errors.push e in
-  let inner_trace,loc,e = match Exninfo.get e ltac_trace_info with
-  | Some (inner_trace,loc) -> inner_trace,loc,e
-  | None ->
-    let loc = match Loc.get_loc e with
-    | None -> Loc.ghost
-    | Some loc -> loc
-    in
-    [], loc, e
+  let inner_trace, e = match Exninfo.get e ltac_trace_info with
+  | Some inner_trace -> inner_trace, e
+  | None -> [], e
   in
   if List.is_empty call_trace && List.is_empty inner_trace then raise e
   else begin
     assert (Errors.noncritical e); (* preserved invariant *)
     let new_trace = inner_trace @ call_trace in
-    let located_exc = Exninfo.add e ltac_trace_info (new_trace, loc) in
+    let located_exc = Exninfo.add e ltac_trace_info new_trace in
     raise located_exc
   end