CI Build UniMath #269
rmatthesbuild-unimath.yml
on: schedule
Sanity Checks
1m 4s
Build on macOS (latest Coq on Homebrew)
1m 17s
Matrix: build-satellites
Matrix: build-Unimath-ubuntu
Annotations
12 errors and 8 warnings
|
Build SetHITs (Coq 8.20)
Universe inconsistency. Cannot enforce UU.u0 <= PartA.cast.u1 because
|
|
Build SetHITs (Coq 8.20)
Universe inconsistency. Cannot enforce UU.u0 <= PartA.cast.u1 because
|
|
Build SetHITs (Coq 8.20)
Universe inconsistency. Cannot enforce UU.u0 <= PartA.cast.u1 because
|
|
Build SetHITs (Coq 8.20)
Universe inconsistency. Cannot enforce UU.u0 <= PartA.cast.u1 because
|
|
Build SetHITs (Coq dev)
Universe inconsistency. Cannot enforce UU.u0 <= PartA.cast.u1 because
|
|
Build SetHITs (Coq dev)
Universe inconsistency. Cannot enforce UU.u0 <= PartA.cast.u1 because
|
|
Build SetHITs (Coq dev)
Universe inconsistency. Cannot enforce UU.u0 <= PartA.cast.u1 because
|
|
Build SetHITs (Coq dev)
Universe inconsistency. Cannot enforce UU.u0 <= PartA.cast.u1 because
|
|
Build Schools (Coq dev)
Use of "Variable" or "Hypothesis" outside sections behaves as
|
|
Build Schools (Coq dev)
Use of "Variable" or "Hypothesis" outside sections behaves as
|
|
Build Schools (Coq 8.20)
Use of "Variable" or "Hypothesis" outside sections behaves as
|
|
Build Schools (Coq 8.20)
Use of "Variable" or "Hypothesis" outside sections behaves as
|
|
Build Schools (Coq dev)
Notation gradth is deprecated. Use isweq_iso instead.
|
|
Build Schools (Coq dev)
Notation gradth is deprecated. Use isweq_iso instead.
|
|
Build Schools (Coq dev)
Notation gradth is deprecated. Use isweq_iso instead.
|
|
Build Schools (Coq dev)
Notation gradth is deprecated. Use isweq_iso instead.
|
|
Build Schools (Coq 8.20)
Notation gradth is deprecated. Use isweq_iso instead.
|
|
Build Schools (Coq 8.20)
Notation gradth is deprecated. Use isweq_iso instead.
|
|
Build Schools (Coq 8.20)
Notation gradth is deprecated. Use isweq_iso instead.
|
|
Build Schools (Coq 8.20)
Notation gradth is deprecated. Use isweq_iso instead.
|