Jean-Christophe Léchenet

After debugging that with the help of Benjamin, it turns out that the problem lies in the parser. The use of `$startpos` and `symbolstartpos` can lead to locations too far...

@vbgl A good first step. I did not look closely at the contents of the files, I guess you did nothing more than just splitting them. Probably the names of...

I think so. The number of dependencies was reduced, but some of them are still there for no good reason. I need to check.

We pushed some nix-related things, that are orthogonal to this PR, because this was convenient. These things are basically the contents of https://github.com/LPCIC/coq-elpi/pull/322. We'll have to decide what to do...

With @bgregoir, we observed that the behaviour in terms of prefix was not consistent between the commands (some seem even buggy). We decided to systematically add an underscore even when...

@gares There is something strange happening with CoqIDE and ProofGeneral (apparently, VsCode works better) due to the fact that there are two _CoqProject files : one for elpi and one...

Indeed, VsCode has the same behaviour as the two others. Actually, there is a problem only with tests, maybe we should add `-R tests elpi.apps.derive.tests` to the inner _CoqProject (or...

@gares done @bgregoir Now you should be able to open the tests files in Proof General without deleting _CoqProject.

I investigated the problems with the tactic `eq_correct_on__solver` (why we need to export things). - We need to export `ssreflect` because otherwise we have the error `Unknown scope delimiting key...

I have the impression you're not so far from merging, nice! I very probably won't have time to look at it before you, though. Unrelated: why did you put me...