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.
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
that came to you indirectly and that does not any more by the removal of "unneeded" dependencies.
I will investigate more precisely asap.