diff options
| author | herbelin | 2013-05-05 22:47:29 +0000 |
|---|---|---|
| committer | herbelin | 2013-05-05 22:47:29 +0000 |
| commit | 21bbdd6b3cea2a2d9763bfc786b56a4b9e95ad06 (patch) | |
| tree | fabf69b850ce65935146a7cb1b86a2ba9c84ceb2 | |
| parent | 86a1787cf9ae815ee8b1f6fd7f39ac615da031a4 (diff) | |
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
| -rw-r--r-- | toplevel/himsg.ml | 10 |
1 files changed, 9 insertions, 1 deletions
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 |