whonore / Coqtail

Interactive Coq Proofs in Vim
MIT License
274 stars 34 forks source link

Adapt to new error location type #358

Closed whonore closed 5 months ago

whonore commented 6 months ago

https://github.com/coq/coq/pull/19040 changes the way error locations are reported in the XML protocol. Specifically, it replaces the loc_s and loc_e attributes of the fail result with an optional Loc.t field. If I understand correctly, the start and stop fields contain the same byte offsets as the old loc_s and loc_e, so it's enough to just extract and return those.