FYI: CI error from MathComp-Analysis

[affeldt-aist]

This is just to bring your attention to the following
CI error in MathComp-Analysis' CI:

https://github.com/math-comp/analysis/actions/runs/11320800077/job/31479254466?pr=1353

It has been triggered by the following PR that just removes unneeded dependencies:

math-comp/analysis#1353

I have not tried to replay SSProve's proof and the probleme might be on MathComp-Analysis'
side but maybe you are relying on the following
command

Obligation Tactic := idtac.

that came to you indirectly and that does not any more by the removal of "unneeded" dependencies.
I will investigate more precisely asap.