Compat with https://github.com/rocq-prover/rocq/pull/19811 #645
Annotations
10 warnings
|
theories/core/sgraph.v#L492
irr_q 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#L488
dis_pq 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/structures.v#L168
rel11 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#L166
rel_sym is declared opaque (Qed) but this is not fully respected
|
|
theories/core/finite_quotient.v#L384
Cast types are ignored in patterns
|
|
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.
|
The logs for this run have expired and are no longer available.
Loading