CI Build UniMath #19
Bigstep22
This run and associated checks have been archived and are scheduled for deletion.
Learn more about checks retention
build-unimath.yml
on: schedule
Sanity Checks
52s
Build on macOS (Coq 8.16)
5m 8s
Matrix: build-satellites
Matrix: build-Unimath-ubuntu
Annotations
2 errors and 22 warnings
|
Build GrpdHITs (Coq dev)
Case analysis on private inductive gquot
|
|
Build GrpdHITs (Coq dev)
Case analysis on private inductive gquot
|
|
Build TypeTheory (Coq dev):
UniMath/Foundations/PartA.v#L350
Declaring arbitrary terms as hints is fragile; it is recommended to
|
|
Build TypeTheory (Coq dev):
UniMath/Foundations/PartA.v#L376
Declaring arbitrary terms as hints is fragile; it is recommended to
|
|
Build SetHITs (Coq dev):
UniMath/Foundations/PartA.v#L350
Declaring arbitrary terms as hints is fragile; it is recommended to
|
|
Build SetHITs (Coq dev):
UniMath/Foundations/PartA.v#L376
Declaring arbitrary terms as hints is fragile; it is recommended to
|
|
Build largecatmodules (Coq dev):
UniMath/Tactics/EnsureStructuredProofs.v#L11
Syntax "Export Set" is deprecated, use the attribute syntax
|
|
Build largecatmodules (Coq dev):
UniMath/Foundations/PartA.v#L350
Declaring arbitrary terms as hints is fragile; it is recommended to
|
|
Build largecatmodules (Coq dev):
UniMath/Foundations/PartA.v#L376
Declaring arbitrary terms as hints is fragile; it is recommended to
|
|
Build GrpdHITs (Coq dev):
UniMath/Tactics/EnsureStructuredProofs.v#L11
Syntax "Export Set" is deprecated, use the attribute syntax
|
|
Build GrpdHITs (Coq dev):
UniMath/Foundations/PartA.v#L350
Declaring arbitrary terms as hints is fragile; it is recommended to
|
|
Build GrpdHITs (Coq dev):
UniMath/Foundations/PartA.v#L376
Declaring arbitrary terms as hints is fragile; it is recommended to
|
|
Build GrpdHITs (Coq dev)
Notation gradth is deprecated. Use isweq_iso instead.
|
|
Build GrpdHITs (Coq dev)
Notation gradth is deprecated. Use isweq_iso instead.
|
|
Build GrpdHITs (Coq dev)
Notation gradth is deprecated. Use isweq_iso instead.
|
|
Build GrpdHITs (Coq dev)
Notation gradth is deprecated. Use isweq_iso instead.
|
|
Build GrpdHITs (Coq dev)
Notation gradth is deprecated. Use isweq_iso instead.
|
|
Build GrpdHITs (Coq dev)
Notation gradth is deprecated. Use isweq_iso instead.
|
|
Build GrpdHITs (Coq dev)
Not a truly recursive fixpoint.
|
|
Build on Linux (Coq dev):
UniMath/Tactics/EnsureStructuredProofs.v#L11
Syntax "Export Set" is deprecated, use the attribute syntax
|
|
Build on Linux (Coq dev):
UniMath/Foundations/PartA.v#L350
Declaring arbitrary terms as hints is fragile; it is recommended to
|
|
Build on Linux (Coq dev):
UniMath/Foundations/PartA.v#L376
Declaring arbitrary terms as hints is fragile; it is recommended to
|
|
Build on Linux (Coq dev):
UniMath/CategoryTheory/Monads/RelMonads_Coreflection.v#L54
ηinv_is_natural is declared opaque (Qed) but this is not fully
|
|
Build on Linux (Coq dev):
UniMath/Bicategories/DaggerCategories/BicatOfDaggerCats.v#L73
DAG_to_cat does not respect the uniform inheritance condition.
|