Pierre Courtieu
Pierre Courtieu
Sorry my question was badly spelled so your answer is now ambiguous :-). Are you saying that when you remove company-coq the bug was still there?
original issue by Vadim Silva on [zulip](https://coq.zulipchat.com/#narrow/stream/304019-Proof-General-users/topic/PG.20does.20not.20position.20to.20error/near/447874951).
Thanks for the reduced case. I am planning a fix for the end of the summer. We need `proof-shell-strip-crs-from-input` for other reasons (#773). FTR, this is also slowed by a...
This needs a bit of a test and discussion. It *seems* to work but it is difficult to be sure. Things to check that I can think of. - Is...
I just added a test that checks that the correct region is highlighted. @hendrik or @erikmd can you review pls? I sum up the fix: Note: testing this I found...
This is not ready yet. I will try to fix this by the end of the summer.
The two failing tests are on coq-8.11. I will try to investigate but maybe this is not blocking. One problem remains: support the coq bug that has just been fixed...
This seems ready. I will merge this tomorrow if no one objects. @erikmd this is an important fix imho, is there something to do to update pg distributed packages?
This PR - fixes #781 - makes use of the character location given by coq instead of the "^^^^" - revealed https://github.com/coq/coq/issues/19355 in coq wrt to error location of curly...
- re-introduced removal of error location from the response buffer. - understood and partially fixed an old small bug on error locations: coq gives wrong location if one insert spaces...