Fix #18657: "Include" objects were not always taken into account in Search

[herbelin]

The fix was simple.

Note that this may imply duplication of results: in the case of a module, we have a result both with the original name and with the included names. But this is a phenomenon which is not only about Include. E.g., Module M := N has similar consequences.

Fixes / closes #18657

• Added / updated test-suite.
• Added changelog.

[Villetaneuse]

That was quick! Thank you very much. The duplication is unfortunate but this can be treated at another time. I'm not even sure there is a better solution; after all the lemmas are there with two names so this behaviour is expected.

[proux01]

@coqbot run full ci

[proux01]

The duplication is unfortunate but this can be treated at another time.

Indeed, nothing specific to the current PR. Still, this duplication remains one of the painful issues of Search IMHO. I guess, outputing only the shortest name would be the best solution in case of duplication.

[herbelin]

I guess, outputing only the shortest name would be the best solution in case of duplication.

Probably, the simplest would be to ensure that the Search is done starting from the most recent declarations and that whenever an Include N (for N a module) or Module M:=N is encountered, N is added to the list of modules to later skip.

[proux01]

There are also Import and Export. Maybe a deduplication mechanism would be enough as a short term solution.

[herbelin]

If I'm not mistaken, the impact of Import and Export on logical declarations is just about how they are made visible in the nametab. Search sees the contents of non-imported modules anyway.

Oh, maybe a simple way is to display only the names whose user name is the same as the canonical name! That could be tried.

[herbelin]

Hum, if we do that, printing only the original "canonical" constants, then this means printing the oldest one, which is probably not the intended, shortly-named, one.

On the other side, if we hide re-aliased module, that's not fully satisfactory either. If we have Module M := N. Module P := N. or Module M := N. Module P := M, we want to give names in P but skip N and M. But that also seems more work.

[proux01]

@coqbot merge now