Adapt to Coq PR #18007: Proof_using.definition_using takes names of fixpoints being built

[herbelin]

This PR is to adapt to Coq PR #18007. Its purpose is to ensure that the kernel does not receive names that are not available in the section.

When building fixpoints, the named context contains the name of the fixpoints being built (not sure this is a good way to do but it is how it is done now). So, we need to tell Proof_using.definition_using to exclude these variables.

I attempted a quick fix for vscoq which is to send to definition_using all the names of proofs being under construction (which are in the LemmaStack iiuc). This is a priori a superset of what is expected by Proof_using.definition_using, but I guess this should do the job.

Don't hesitate to propose another fix.

In any case, this is to be merged synchronously with coq/coq#18007.

[ppedrot]

Please merge now.

[SkySkimmer]

ping

[SkySkimmer]

ping

or add @coq-community/coq-overlay-mergers to allowed mergers on this repo

[ppedrot]

Ping @rtetley explicitly just in case.

[rtetley]

Sorry, missed this one, I'll be sure to track the PR next time. However this seems to be failing ?

[SkySkimmer]

I guess CI wasn't run since the upstream PR was merged

[SkySkimmer]

Some of the CI jobs are running the wrong coq version

File "dm/completionSuggester.ml", line 424, characters 2-23:
424 |   Search.generic_search env sigma display;
        ^^^^^^^^^^^^^^^^^^^^^
Error: This function has type Environ.env -> Search.display_function -> unit
       It is applied to too many arguments; maybe you forgot a `;'.