Compile with mathcomp 2.3.0 #18
Annotations
10 warnings
|
Run coq-community/docker-coq-action@v1:
dioid.v#L76
Notation idempotent is deprecated since mathcomp 2.3.0.
|
|
Run coq-community/docker-coq-action@v1:
dioid.v#L108
Notation idempotent is deprecated since mathcomp 2.3.0.
|
|
Run coq-community/docker-coq-action@v1:
dioid.v#L127
Notation idempotent is deprecated since mathcomp 2.3.0.
|
|
Run coq-community/docker-coq-action@v1:
dioid.v#L171
Notation idempotent is deprecated since mathcomp 2.3.0.
|
|
Run coq-community/docker-coq-action@v1:
dioid.v#L244
Notation idempotent is deprecated since mathcomp 2.3.0.
|
|
Run coq-community/docker-coq-action@v1:
dioid.v#L280
Notation idempotent is deprecated since mathcomp 2.3.0.
|
|
Run coq-community/docker-coq-action@v1:
dioid.v#L331
Notation idempotent is deprecated since mathcomp 2.3.0.
|
|
Run coq-community/docker-coq-action@v1:
dioid.v#L334
Reference leEsub is deprecated since mathcomp 2.3.0.
|
|
Run coq-community/docker-coq-action@v1:
dioid.v#L334
Reference leEsub is deprecated since mathcomp 2.3.0.
|
|
Run coq-community/docker-coq-action@v1:
dioid.v#L334
Reference leEsub is deprecated since mathcomp 2.3.0.
|
Loading