Bumped version number to 2.16 #1208
andrew-appelAnnotations
1 error and 90 warnings
|
test (dev, test3, 32)
(in proof G2_2_3_equiv): Attempt to save an incomplete proof
|
|
build (dev, 32, vst):
msl/sepalg_functors.v#L86
Using "..." is deprecated, use "; auto." instead
|
|
build (dev, 32, vst):
msl/sepalg_functors.v#L84
Using "..." is deprecated, use "; auto." instead
|
|
build (dev, 32, vst):
msl/sepalg_functors.v#L82
Using "..." is deprecated, use "; auto." instead
|
|
build (dev, 32, vst):
msl/psepalg.v#L36
Using "..." is deprecated, use "; eauto." instead
|
|
build (dev, 32, vst):
msl/psepalg.v#L34
Using "..." is deprecated, use "; eauto." instead
|
|
build (dev, 32, vst):
msl/sepalg.v#L702
Using "..." is deprecated, use "; auto." instead
|
|
build (dev, 32, vst):
msl/eq_dec.v#L50
Using "..." is deprecated, use "; auto." instead
|
|
build (dev, 32, vst):
msl/eq_dec.v#L47
Using "..." is deprecated, use "; auto." instead
|
|
build (dev, 32, vst):
msl/eq_dec.v#L29
Using "..." is deprecated, use "; auto." instead
|
|
build (dev, 32, vst):
msl/eq_dec.v#L27
Using "..." is deprecated, use "; auto." instead
|
|
build (dev, 64, vst):
msl/sepalg_functors.v#L86
Using "..." is deprecated, use "; auto." instead
|
|
build (dev, 64, vst):
msl/sepalg_functors.v#L84
Using "..." is deprecated, use "; auto." instead
|
|
build (dev, 64, vst):
msl/sepalg_functors.v#L82
Using "..." is deprecated, use "; auto." instead
|
|
build (dev, 64, vst):
msl/psepalg.v#L36
Using "..." is deprecated, use "; eauto." instead
|
|
build (dev, 64, vst):
msl/psepalg.v#L34
Using "..." is deprecated, use "; eauto." instead
|
|
build (dev, 64, vst):
msl/sepalg.v#L702
Using "..." is deprecated, use "; auto." instead
|
|
build (dev, 64, vst):
msl/eq_dec.v#L50
Using "..." is deprecated, use "; auto." instead
|
|
build (dev, 64, vst):
msl/eq_dec.v#L47
Using "..." is deprecated, use "; auto." instead
|
|
build (dev, 64, vst):
msl/eq_dec.v#L29
Using "..." is deprecated, use "; auto." instead
|
|
build (dev, 64, vst):
msl/eq_dec.v#L27
Using "..." is deprecated, use "; auto." instead
|
|
test (dev, test2, 64)
Use of "Notation" keyword for abbreviations is deprecated, use
|
|
test (dev, test2, 64)
Use of "Notation" keyword for abbreviations is deprecated, use
|
|
test (dev, test2, 64)
Use of "Notation" keyword for abbreviations is deprecated, use
|
|
test (dev, test2, 64)
Use of "Notation" keyword for abbreviations is deprecated, use
|
|
test (dev, test2, 64)
Use of "Notation" keyword for abbreviations is deprecated, use
|
|
test (dev, test2, 64)
Use of "Notation" keyword for abbreviations is deprecated, use
|
|
test (dev, test2, 64)
Use of "Notation" keyword for abbreviations is deprecated, use
|
|
test (dev, test2, 64)
Use of "Notation" keyword for abbreviations is deprecated, use
|
|
test (dev, test2, 64)
"From Coq" has been replaced by "From Stdlib".
|
|
test (dev, test2, 64)
"From Coq" has been replaced by "From Stdlib".
|
|
test (dev, test4, 64)
Hint Db norm already exists and is discriminated.
|
|
test (dev, test4, 64)
Hint Db norm already exists and is discriminated.
|
|
test (dev, test4, 64)
Hint Db norm already exists and is discriminated.
|
|
test (dev, test4, 64)
Hint Db norm already exists and is discriminated.
|
|
test (dev, test4, 64)
Hint Db norm already exists and is discriminated.
|
|
test (dev, test4, 64)
Hint Db norm already exists and is discriminated.
|
|
test (dev, test4, 64)
Hint Db norm already exists and is discriminated.
|
|
test (dev, test4, 64)
Hint Db norm already exists and is discriminated.
|
|
test (dev, test4, 64)
Use of "Notation" keyword for abbreviations is deprecated, use
|
|
test (dev, test4, 64)
Hint Db norm already exists and is discriminated.
|
|
test (dev, test5, 64)
Hint Db norm already exists and is discriminated.
|
|
test (dev, test5, 64)
Hint Db norm already exists and is discriminated.
|
|
test (dev, test5, 64)
Hint Db norm already exists and is discriminated.
|
|
test (dev, test5, 64)
Hint Db norm already exists and is discriminated.
|
|
test (dev, test5, 64)
Hint Db norm already exists and is discriminated.
|
|
test (dev, test5, 64)
Hint Db norm already exists and is discriminated.
|
|
test (dev, test5, 64)
Hint Db norm already exists and is discriminated.
|
|
test (dev, test5, 64)
Hint Db norm already exists and is discriminated.
|
|
test (dev, test5, 64)
Hint Db norm already exists and is discriminated.
|
|
test (dev, test5, 64)
Hint Db norm already exists and is discriminated.
|
|
test (dev, test2, 32)
Use of "Notation" keyword for abbreviations is deprecated, use
|
|
test (dev, test2, 32)
Use of "Notation" keyword for abbreviations is deprecated, use
|
|
test (dev, test2, 32)
Use of "Notation" keyword for abbreviations is deprecated, use
|
|
test (dev, test2, 32)
Use of "Notation" keyword for abbreviations is deprecated, use
|
|
test (dev, test2, 32)
Use of "Notation" keyword for abbreviations is deprecated, use
|
|
test (dev, test2, 32)
Use of "Notation" keyword for abbreviations is deprecated, use
|
|
test (dev, test2, 32)
Use of "Notation" keyword for abbreviations is deprecated, use
|
|
test (dev, test2, 32)
Use of "Notation" keyword for abbreviations is deprecated, use
|
|
test (dev, test2, 32)
"From Coq" has been replaced by "From Stdlib".
|
|
test (dev, test2, 32)
"From Coq" has been replaced by "From Stdlib".
|
|
test (dev, test, 64)
Hint Db norm already exists and is discriminated.
|
|
test (dev, test, 64)
Hint Db norm already exists and is discriminated.
|
|
test (dev, test, 64)
Hint Db norm already exists and is discriminated.
|
|
test (dev, test, 64)
Hint Db norm already exists and is discriminated.
|
|
test (dev, test, 64)
Hint Db norm already exists and is discriminated.
|
|
test (dev, test, 64)
Hint Db norm already exists and is discriminated.
|
|
test (dev, test, 64)
Hint Db norm already exists and is discriminated.
|
|
test (dev, test, 64)
Implicitly declaring Rewrite hint databases is deprecated. Please
|
|
test (dev, test, 64)
Hint Db norm already exists and is discriminated.
|
|
test (dev, test, 64)
Hint Db norm already exists and is discriminated.
|
|
test (dev, test3, 32)
Loading Stdlib without prefix is deprecated.
|
|
test (dev, test3, 32)
Loading Stdlib without prefix is deprecated.
|
|
test (dev, test3, 32)
Loading Stdlib without prefix is deprecated.
|
|
test (dev, test3, 32)
Loading Stdlib without prefix is deprecated.
|
|
test (dev, test3, 32)
Loading Stdlib without prefix is deprecated.
|
|
test (dev, test3, 32)
"From Coq" has been replaced by "From Stdlib".
|
|
test (dev, test3, 32)
"From Coq" has been replaced by "From Stdlib".
|
|
test (dev, test3, 32)
Loading Stdlib without prefix is deprecated.
|
|
test (dev, test3, 32)
Implicitly declaring Rewrite hint databases is deprecated. Please
|
|
test (dev, test3, 32)
Loading Stdlib without prefix is deprecated.
|
|
test (dev, test, 32)
In term, tolerating this expression at a higher level than expected.
|
|
test (dev, test, 32)
In term, tolerating this expression at a higher level than expected.
|
|
test (dev, test, 32)
In term, tolerating this expression at a higher level than expected.
|
|
test (dev, test, 32)
In term, tolerating this expression at a higher level than expected.
|
|
test (dev, test, 32)
In term, tolerating this expression at a higher level than expected.
|
|
test (dev, test, 32)
In term, tolerating this expression at a higher level than expected.
|
|
test (dev, test, 32)
In term, tolerating this expression at a higher level than expected.
|
|
test (dev, test, 32)
In term, tolerating this expression at a higher level than expected.
|
|
test (dev, test, 32)
Hint Db norm already exists and is discriminated.
|
|
test (dev, test, 32)
Hint Db norm already exists and is discriminated.
|
Artifacts
Produced during runtime
| Name | Size | Digest | |
|---|---|---|---|
|
VST build artifacts dev 32
Expired
|
114 MB |
sha256:38e3040c48b747b4c16c77ddd096cb878c4e7a1715f3c2790fa44885f9b10287
|
|
|
VST build artifacts dev 64
Expired
|
114 MB |
sha256:b49f5614978067444bdc100378ad7b0fb51b8c252d0bf3bea59e67a10dbab748
|
|