Skip to content
CI

Compile with mathcomp 2.3.0 #18

Sign in to view logs

Compile with mathcomp 2.3.0

Compile with mathcomp 2.3.0 #18

Triggered via push February 24, 2025 16:38
@proux01proux01
pushed 0e6e3c9
master
Status Success
Total duration 6m 20s
Artifacts –

coq-action.yml

on: push
Matrix: build
Fit to window
Zoom out
Zoom in

Annotations

10 warnings
build (mathcomp/mathcomp:2.3.0-coq-8.20): dioid.v#L76
Notation idempotent is deprecated since mathcomp 2.3.0.
build (mathcomp/mathcomp:2.3.0-coq-8.20): dioid.v#L108
Notation idempotent is deprecated since mathcomp 2.3.0.
build (mathcomp/mathcomp:2.3.0-coq-8.20): dioid.v#L127
Notation idempotent is deprecated since mathcomp 2.3.0.
build (mathcomp/mathcomp:2.3.0-coq-8.20): dioid.v#L171
Notation idempotent is deprecated since mathcomp 2.3.0.
build (mathcomp/mathcomp:2.3.0-coq-8.20): dioid.v#L244
Notation idempotent is deprecated since mathcomp 2.3.0.
build (mathcomp/mathcomp:2.3.0-coq-8.20): dioid.v#L280
Notation idempotent is deprecated since mathcomp 2.3.0.
build (mathcomp/mathcomp:2.3.0-coq-8.20): dioid.v#L331
Notation idempotent is deprecated since mathcomp 2.3.0.
build (mathcomp/mathcomp:2.3.0-coq-8.20): dioid.v#L334
Reference leEsub is deprecated since mathcomp 2.3.0.
build (mathcomp/mathcomp:2.3.0-coq-8.20): dioid.v#L334
Reference leEsub is deprecated since mathcomp 2.3.0.
build (mathcomp/mathcomp:2.3.0-coq-8.20): dioid.v#L334
Reference leEsub is deprecated since mathcomp 2.3.0.