Adapt to https://github.com/math-comp/math-comp/pull/1352 #217
Annotations
10 warnings
|
theories/xmathcomp/various.v#L164
HB: no new instance is generated
|
|
theories/xmathcomp/various.v#L252
Notation comRingType is deprecated since mathcomp 2.4.0.
|
|
theories/xmathcomp/various.v#L259
Notation ringType is deprecated since mathcomp 2.4.0.
|
|
theories/xmathcomp/various.v#L301
Notation ringType is deprecated since mathcomp 2.4.0.
|
|
theories/xmathcomp/various.v#L318
Notation ringType is deprecated since mathcomp 2.4.0.
|
|
theories/xmathcomp/various.v#L322
Notation size_opp is deprecated since mathcomp 2.4.0.
|
|
theories/xmathcomp/various.v#L322
Notation size_opp is deprecated since mathcomp 2.4.0.
|
|
theories/xmathcomp/various.v#L322
Notation size_opp is deprecated since mathcomp 2.4.0.
|
|
theories/xmathcomp/various.v#L325
Notation ringType is deprecated since mathcomp 2.4.0.
|
|
theories/xmathcomp/various.v#L329
Notation ringType is deprecated since mathcomp 2.4.0.
|
The logs for this run have expired and are no longer available.
Loading