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 /plugins/xml/xmlcommand.ml | |
| 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
Diffstat (limited to 'plugins/xml/xmlcommand.ml')
0 files changed, 0 insertions, 0 deletions