CI Build UniMath #124
benediktahrensbuild-unimath.yml
on: schedule
Assemble the site
26s
Annotations
60 warnings
|
Build Schools (Coq dev):
UniMath/Foundations/PartA.v#L350
Implicitly declaring hint databases is deprecated. Please explicitly
|
|
Build Schools (Coq dev):
UniMath/Foundations/Preamble.v#L144
Use of "Notation" keyword for abbreviations is deprecated, use
|
|
Build Schools (Coq dev):
UniMath/Foundations/Preamble.v#L141
Implicitly declaring hint databases is deprecated. Please explicitly
|
|
Build Schools (Coq dev):
UniMath/Foundations/Preamble.v#L50
Use of "Notation" keyword for abbreviations is deprecated, use
|
|
Build Schools (Coq dev):
UniMath/Foundations/Preamble.v#L49
Use of "Notation" keyword for abbreviations is deprecated, use
|
|
Build Schools (Coq dev):
UniMath/Foundations/Init.v#L94
Postfix notations (i.e. starting with a nonterminal symbol and
|
|
Build Schools (Coq dev):
UniMath/Foundations/Init.v#L65
Closed notations (i.e. starting and ending with a terminal symbol)
|
|
Build Schools (Coq dev):
UniMath/Foundations/Init.v#L61
Postfix notations (i.e. starting with a nonterminal symbol and
|
|
Build Schools (Coq dev):
UniMath/Foundations/Init.v#L6
"From Coq" has been replaced by "From Stdlib".
|
|
Build Schools (Coq dev):
UniMath/Foundations/Init.v#L3
"From Coq" has been replaced by "From Stdlib".
|
|
Build SetHITs (Coq dev):
UniMath/Foundations/PartA.v#L350
Implicitly declaring hint databases is deprecated. Please explicitly
|
|
Build SetHITs (Coq dev):
UniMath/Foundations/Preamble.v#L144
Use of "Notation" keyword for abbreviations is deprecated, use
|
|
Build SetHITs (Coq dev):
UniMath/Foundations/Preamble.v#L141
Implicitly declaring hint databases is deprecated. Please explicitly
|
|
Build SetHITs (Coq dev):
UniMath/Foundations/Preamble.v#L50
Use of "Notation" keyword for abbreviations is deprecated, use
|
|
Build SetHITs (Coq dev):
UniMath/Foundations/Preamble.v#L49
Use of "Notation" keyword for abbreviations is deprecated, use
|
|
Build SetHITs (Coq dev):
UniMath/Foundations/Init.v#L94
Postfix notations (i.e. starting with a nonterminal symbol and
|
|
Build SetHITs (Coq dev):
UniMath/Foundations/Init.v#L65
Closed notations (i.e. starting and ending with a terminal symbol)
|
|
Build SetHITs (Coq dev):
UniMath/Foundations/Init.v#L61
Postfix notations (i.e. starting with a nonterminal symbol and
|
|
Build SetHITs (Coq dev):
UniMath/Foundations/Init.v#L6
"From Coq" has been replaced by "From Stdlib".
|
|
Build SetHITs (Coq dev):
UniMath/Foundations/Init.v#L3
"From Coq" has been replaced by "From Stdlib".
|
|
Build TypeTheory (Coq dev):
UniMath/Foundations/PartA.v#L350
Implicitly declaring hint databases is deprecated. Please explicitly
|
|
Build TypeTheory (Coq dev):
UniMath/Foundations/Preamble.v#L144
Use of "Notation" keyword for abbreviations is deprecated, use
|
|
Build TypeTheory (Coq dev):
UniMath/Foundations/Preamble.v#L141
Implicitly declaring hint databases is deprecated. Please explicitly
|
|
Build TypeTheory (Coq dev):
UniMath/Foundations/Preamble.v#L50
Use of "Notation" keyword for abbreviations is deprecated, use
|
|
Build TypeTheory (Coq dev):
UniMath/Foundations/Preamble.v#L49
Use of "Notation" keyword for abbreviations is deprecated, use
|
|
Build TypeTheory (Coq dev):
UniMath/Foundations/Init.v#L94
Postfix notations (i.e. starting with a nonterminal symbol and
|
|
Build TypeTheory (Coq dev):
UniMath/Foundations/Init.v#L65
Closed notations (i.e. starting and ending with a terminal symbol)
|
|
Build TypeTheory (Coq dev):
UniMath/Foundations/Init.v#L61
Postfix notations (i.e. starting with a nonterminal symbol and
|
|
Build TypeTheory (Coq dev):
UniMath/Foundations/Init.v#L6
"From Coq" has been replaced by "From Stdlib".
|
|
Build TypeTheory (Coq dev):
UniMath/Foundations/Init.v#L3
"From Coq" has been replaced by "From Stdlib".
|
|
Build largecatmodules (Coq dev):
UniMath/Foundations/PartA.v#L350
Implicitly declaring hint databases is deprecated. Please explicitly
|
|
Build largecatmodules (Coq dev):
UniMath/Foundations/Preamble.v#L144
Use of "Notation" keyword for abbreviations is deprecated, use
|
|
Build largecatmodules (Coq dev):
UniMath/Foundations/Preamble.v#L141
Implicitly declaring hint databases is deprecated. Please explicitly
|
|
Build largecatmodules (Coq dev):
UniMath/Foundations/Preamble.v#L50
Use of "Notation" keyword for abbreviations is deprecated, use
|
|
Build largecatmodules (Coq dev):
UniMath/Foundations/Preamble.v#L49
Use of "Notation" keyword for abbreviations is deprecated, use
|
|
Build largecatmodules (Coq dev):
UniMath/Foundations/Init.v#L94
Postfix notations (i.e. starting with a nonterminal symbol and
|
|
Build largecatmodules (Coq dev):
UniMath/Foundations/Init.v#L65
Closed notations (i.e. starting and ending with a terminal symbol)
|
|
Build largecatmodules (Coq dev):
UniMath/Foundations/Init.v#L61
Postfix notations (i.e. starting with a nonterminal symbol and
|
|
Build largecatmodules (Coq dev):
UniMath/Foundations/Init.v#L6
"From Coq" has been replaced by "From Stdlib".
|
|
Build largecatmodules (Coq dev):
UniMath/Foundations/Init.v#L3
"From Coq" has been replaced by "From Stdlib".
|
|
Build GrpdHITs (Coq dev):
UniMath/Foundations/PartA.v#L350
Implicitly declaring hint databases is deprecated. Please explicitly
|
|
Build GrpdHITs (Coq dev):
UniMath/Foundations/Preamble.v#L144
Use of "Notation" keyword for abbreviations is deprecated, use
|
|
Build GrpdHITs (Coq dev):
UniMath/Foundations/Preamble.v#L141
Implicitly declaring hint databases is deprecated. Please explicitly
|
|
Build GrpdHITs (Coq dev):
UniMath/Foundations/Preamble.v#L50
Use of "Notation" keyword for abbreviations is deprecated, use
|
|
Build GrpdHITs (Coq dev):
UniMath/Foundations/Preamble.v#L49
Use of "Notation" keyword for abbreviations is deprecated, use
|
|
Build GrpdHITs (Coq dev):
UniMath/Foundations/Init.v#L94
Postfix notations (i.e. starting with a nonterminal symbol and
|
|
Build GrpdHITs (Coq dev):
UniMath/Foundations/Init.v#L65
Closed notations (i.e. starting and ending with a terminal symbol)
|
|
Build GrpdHITs (Coq dev):
UniMath/Foundations/Init.v#L61
Postfix notations (i.e. starting with a nonterminal symbol and
|
|
Build GrpdHITs (Coq dev):
UniMath/Foundations/Init.v#L6
"From Coq" has been replaced by "From Stdlib".
|
|
Build GrpdHITs (Coq dev):
UniMath/Foundations/Init.v#L3
"From Coq" has been replaced by "From Stdlib".
|
|
Build on Linux (Coq dev):
UniMath/Foundations/PartA.v#L350
Implicitly declaring hint databases is deprecated. Please explicitly
|
|
Build on Linux (Coq dev):
UniMath/Foundations/Preamble.v#L144
Use of "Notation" keyword for abbreviations is deprecated, use
|
|
Build on Linux (Coq dev):
UniMath/Foundations/Preamble.v#L141
Implicitly declaring hint databases is deprecated. Please explicitly
|
|
Build on Linux (Coq dev):
UniMath/Foundations/Preamble.v#L50
Use of "Notation" keyword for abbreviations is deprecated, use
|
|
Build on Linux (Coq dev):
UniMath/Foundations/Preamble.v#L49
Use of "Notation" keyword for abbreviations is deprecated, use
|
|
Build on Linux (Coq dev):
UniMath/Foundations/Init.v#L94
Postfix notations (i.e. starting with a nonterminal symbol and
|
|
Build on Linux (Coq dev):
UniMath/Foundations/Init.v#L65
Closed notations (i.e. starting and ending with a terminal symbol)
|
|
Build on Linux (Coq dev):
UniMath/Foundations/Init.v#L61
Postfix notations (i.e. starting with a nonterminal symbol and
|
|
Build on Linux (Coq dev):
UniMath/Foundations/Init.v#L6
"From Coq" has been replaced by "From Stdlib".
|
|
Build on Linux (Coq dev):
UniMath/Foundations/Init.v#L3
"From Coq" has been replaced by "From Stdlib".
|
Artifacts
Produced during runtime
| Name | Size | Digest | |
|---|---|---|---|
|
rocqdoc
|
16.8 MB |
sha256:45e2a75352538723c10044e9f5af1df6255b21d5b2680ee84b41f9e9a6f07053
|
|