aboutsummaryrefslogtreecommitdiff
path: root/dev
diff options
context:
space:
mode:
authorMaxime Dénès2016-06-16 02:24:54 +0200
committerMaxime Dénès2016-06-20 15:05:19 +0200
commit058209a96579c73d786a3ceb8a7445cd5b7a8962 (patch)
tree26fff33cc21e976a4b82446b7296f74fe730d30f /dev
parenta8088f565da008d3b1780f38de0ee894e8fd0baa (diff)
Add file name, line number and beginning of line position to locations.
Coq locations already had support for this, but were containing dummy information. We now don't need anymore to reconstruct this information by browsing the file when printing an error message or enriching exceptions on the fly. It also became easier to interface with Coq since locations emitted by the lexer now always contain full information. On the API side, Loc.represent disappeared and Loc.t is now exposed as record. It is less error-prone than manipulating a tuple of 5 integers. Also, Loc.create takes 5 arguments instead of 3 and a pair.
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions