Adapt to https://github.com/coq/coq/pull/19530 #52
Annotations
10 warnings
|
theories/Core/RelDec.v#L1
Coq.Bool.Bool has been replaced by Stdlib.Bool.Bool.
|
|
theories/Core/RelDec.v#L2
Coq.Classes.RelationClasses has been replaced by
|
|
theories/Core/RelDec.v#L3
Coq.Setoids.Setoid has been replaced by Stdlib.Setoids.Setoid.
|
|
theories/Core/EquivDec.v#L1
Coq.Classes has been replaced by Stdlib.Classes.
|
|
theories/Core/Decision.v#L1
Coq.Classes has been replaced by Stdlib.Classes.
|
|
theories/Structures/Monoid.v#L16
Automatically putting MonoidLaws in Prop even though it was declared
|
|
theories/Data/PreFun.v#L1
Coq.Classes has been replaced by Stdlib.Classes.
|
|
theories/Data/PreFun.v#L2
Coq.Relations has been replaced by Stdlib.Relations.
|
|
theories/Data/ListNth.v#L1
Coq.Lists has been replaced by Stdlib.Lists.
|
|
theories/Data/ListNth.v#L2
Coq.Arith has been replaced by Stdlib.Arith.
|
This job succeeded
Loading