In this way the line number in the loc is not reset to 0. This has no use internally, since the document holds the text and computes line number correctly, but Coq code and plugins may want to display a loc (with a correct line number).
Note that the char-number is correct, since it comes from the stream, apparently.
This makes errors reported by Coq-Elpi more precise.
In this way the line number in the loc is not reset to 0. This has no use internally, since the document holds the text and computes line number correctly, but Coq code and plugins may want to display a loc (with a correct line number).
Note that the char-number is correct, since it comes from the stream, apparently.
This makes errors reported by Coq-Elpi more precise.