change boilerplate for 8.19 and beyond #44
Annotations
7 warnings
|
tutorial_type_classes/SRC/EMonoid.v#L7
A coercion will be introduced instead of an instance in future
|
|
tutorial_type_classes/SRC/Monoid_op_classes.v#L319
A coercion will be introduced instead of an instance in future
|
|
tutorial_type_classes/SRC/Monoid_op_classes.v#L442
A coercion will be introduced instead of an instance in future
|
|
tutorial_type_classes/SRC/Monoid_op_classes.v#L443
A coercion will be introduced instead of an instance in future
|
|
tutorial_type_classes/SRC/Monoid_op_classes.v#L464
A coercion will be introduced instead of an instance in future
|
|
tutorial_type_classes/SRC/Monoid_op_classes.v#L468
A coercion will be introduced instead of an instance in future
|
|
ch8_inductive_predicates/SRC/magaud.v#L34
nu_constant is declared opaque (Qed) but this is not fully respected
|
The logs for this run have expired and are no longer available.
Loading