From 21bbdd6b3cea2a2d9763bfc786b56a4b9e95ad06 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sun, 5 May 2013 22:47:29 +0000
Subject: Improvement of r16204 on reporting tactic error locations: if the
 main error is not located, then do not use locations from Tactic Notation
 (TacAlias) or TACTIC EXTEND (TacExtend) code since they are relative to the
 defining code of these extensions.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16468 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 toplevel/himsg.ml | 10 +++++++++-
 1 file changed, 9 insertions(+), 1 deletion(-)

diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index dc906d281a..afd04f8b91 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -1099,6 +1099,14 @@ let explain_ltac_call_trace (nrep,last,trace,loc) =
   else
     mt ()
 
+let skip_extensions trace =
+  let rec aux = function
+  | (_,_,Proof_type.LtacAtomCall
+      (Tacexpr.TacAlias _ | Tacexpr.TacExtend _) as tac) :: tail -> [tac]
+  | _ :: tail -> aux tail
+  | [] -> [] in
+  List.rev (aux (List.rev trace))
+
 let extract_ltac_trace trace eloc =
   let (nrep,loc,c),tail = List.sep_last trace in
   if is_defined_ltac trace then
@@ -1116,5 +1124,5 @@ let extract_ltac_trace trace eloc =
         | (_,loc,_)::tail when not (Loc.is_ghost loc) -> loc
         | _::tail -> aux tail
         | [] -> Loc.ghost in
-        aux trace in
+        aux (skip_extensions trace) in
     None, best_loc
-- 
cgit v1.2.3