Finally, I found the reason for the bad location reporting using unicode in the xml protocol (thus e.g. in CoqIDE): there was a remaining place where line numbers were not serialized. I'm going to make a PR.
Last updated: Oct 13 2024 at 01:02 UTC