[toc] [petanque] Definition shadowing makes API hard to use.

[ejgallego]

Originally reported by @gbdrt via mail.

In Flèche's TOC, we don't track scope of names, so in some cases shadowing happens. For example, in the following file:

Definition a := 3.

Section Bar.

Hypothesis (a : nat).

....

End Bar.

a in the section will shadow the first definition.

I wonder what the best remedy is here, other than the already planned fix for #332 , maybe we can hotfix this by qualifying hypothesis with their section name? (tho this results in some weird setup)

In general, Coq namespace semantics are a bit strange so it is not easy to mirror them easily in our TOC.

In general, I'm not sure how to make the naming in the start API fully reliable. We could allow for a document position, but that also has its own problems (how is the client going to resolve name to a position anyways)

cc #322

[gbdrt]

Somehow this is not visible in coq-lsp. A file with a similar structure can be checked without errors.

[ejgallego]

Indeed, this is not really an error, but more like the map from names to locations we are using (toc for "table of contents") returns the latter location.

To solve this, we need to figure out a way to disambiguate that.

[ejgallego]

To fix the test for now I'd suggest renaming the hypothesis that is shadowing the lemma. But indeed, that's such a PITA.