Adapt to mathc-omp/math-comp#1240 #606
Annotations
11 warnings
|
The following actions uses Node.js version which is deprecated and will be forced to run on node20: actions/checkout@v3. For more info: https://github.blog/changelog/2024-03-07-github-actions-all-actions-will-run-on-node20-instead-of-node16-by-default/
|
|
theories/core/arc.v#L263
Notation sub is deprecated since mathcomp 2.0.0. Use Sub instead.
|
|
theories/core/arc.v#L263
Notation sub is deprecated since mathcomp 2.0.0. Use Sub instead.
|
|
theories/core/finite_quotient.v#L384
Cast types are ignored in patterns
|
|
theories/core/structures.v#L166
rel_sym is declared opaque (Qed) but this is not fully respected
|
|
theories/core/structures.v#L167
rel01 is declared opaque (Qed) but this is not fully respected
|
|
theories/core/structures.v#L168
rel11 is declared opaque (Qed) but this is not fully respected
|
|
theories/core/ptt.v#L147
tm_eqv_eqv is declared opaque (Qed) but this is not fully respected
|
|
theories/core/sgraph.v#L488
dis_pq is declared opaque (Qed) but this is not fully respected
|
|
theories/core/sgraph.v#L490
irr_p is declared opaque (Qed) but this is not fully respected
|
|
theories/core/sgraph.v#L492
irr_q is declared opaque (Qed) but this is not fully respected
|
This job succeeded
Loading