HITs: fix inconsistencies from several HITs #1563
Annotations
10 warnings
|
theories/Basics/Equivalences.v#L104
adj is declared opaque (Qed) but this is not fully respected inside
|
|
theories/Colimits/Pushout.v#L281
esp1_beta_pglue is declared opaque (Qed) but this is not fully
|
|
theories/Colimits/Pushout.v#L300
esp2_beta_pglue is declared opaque (Qed) but this is not fully
|
|
theories/Classes/implementations/peano_naturals.v#L22
natpaths_symm is declared opaque (Qed) but this is not fully
|
|
theories/Classes/implementations/peano_naturals.v#L586
f_preserves_0 is declared opaque (Qed) but this is not fully
|
|
theories/Classes/implementations/peano_naturals.v#L589
f_preserves_1 is declared opaque (Qed) but this is not fully
|
|
theories/Classes/implementations/peano_naturals.v#L596
f_S is declared opaque (Qed) but this is not fully respected inside
|
|
theories/Classes/implementations/peano_naturals.v#L606
f_preserves_plus is declared opaque (Qed) but this is not fully
|
|
theories/Classes/implementations/peano_naturals.v#L618
f_preserves_mult is declared opaque (Qed) but this is not fully
|
|
theories/Classes/implementations/binary_naturals.v#L71
succunary is declared opaque (Qed) but this is not fully respected
|
The logs for this run have expired and are no longer available.
Loading