coq-dpdgraph icon indicating copy to clipboard operation
coq-dpdgraph copied to clipboard

feature request: add location info in the dpd file

Open hendriktews opened this issue 8 years ago • 0 comments

The dpd file should contain line number and/or character position information and dpdusage should print it in a popular error message format, such that any decent editor can visit items in the result list of dpdusage directly.

hendriktews avatar Feb 27 '17 20:02 hendriktews