[coq] Adapt to rocq-prover/rocq#20601

[ejgallego]

trafficstars

[ejgallego]

@SkySkimmer CI fails with:

"message": "Unable to locate library a (while searching for a .vos file)."

I can of course fix the test, but I'm not sure the new message is good, previous one was:

"message": "Cannot find a physical path bound to logical path a."

[ejgallego]

[fixed the CI meanwhile so you can get a green CI upstream]

[SkySkimmer]

The message change is semi-deliberate (it makes the implem simpler and seems correct).

TBH IDK why we have 2 messages for failing to find a library.

[ejgallego]

The message change is semi-deliberate (it makes the implem simpler and seems correct).

TBH IDK why we have 2 messages for failing to find a library.

Indeed I think the change is a good one, what I find a bit confusing is the "searching for .vos", not sure this is relevant for users.

CI failures are not important (web is because I need to use the waterproof overlay, as the web version includes waterproof)

[proux01]

Upstream PR merged, this can be merged

[SkySkimmer]

sign the commit (-S option to git commit) to be mergeable