Pierre Courtieu
Pierre Courtieu
Any idea about this?
I could indeed trace the problem to this line https://github.com/coq/coq/blame/3c5387245ab14d1520967184c8fab49b3676a2b4/tactics/tactics.ml#L2963C6-L2963C6 ```ocaml (* Instantiate unsolved holes with their default value *) let fold sigma (env, ev) = if isEvar sigma ev...
#18341 being abandoned this needs some fix or nofix.
#15244 is fixed but this bug is sill there. `as H` is supported, `as h%H` is supported, but not `as H%H4`, i.e. only when the name of the hypothesis is...
This setting dates back the times when coqtop would duplicate its prompt after each newline input ad de-synch PG. I don't know exactly when this behaviour disappeared from the `coqtop...
Yes. Let us test what the ci says about that.
I can't have look now but it is strange: replacing each `\n` by a space should not change the computation of (char) positions of errors...
Had a quick look. Here are the elements: - Coq error reporting in coqtop is such that the error message only cites the **line** containing the error, not the entire...
The error location is now parsed as said above (PR #781) we can close this issue again I guess.
I second this feature wish. Someone knows how difficult this would be?