Port VST 2.x to CompCert master #1078
andrew-appelAnnotations
8 errors and 16 warnings
|
build (8.19, 32, vst)
The run was canceled by @andrew-appel.
|
|
build (8.19, 32, vst)
The operation was canceled.
|
|
build (8.18, 64, vst)
The run was canceled by @andrew-appel.
|
|
build (8.18, 64, vst)
The operation was canceled.
|
|
build (8.19, 64, vst)
The run was canceled by @andrew-appel.
|
|
build (8.19, 64, vst)
The operation was canceled.
|
|
build (dev, 64, vst)
The run was canceled by @andrew-appel.
|
|
build (dev, 64, vst)
The operation was canceled.
|
|
build (8.19, 32, vst):
compcert/lib/IEEE754_extra.v#L434
Notation IZR_neq is deprecated since 8.19.
|
|
build (8.19, 32, vst):
compcert/lib/IEEE754_extra.v#L434
Notation IZR_neq is deprecated since 8.19.
|
|
build (8.18, 64, vst):
compcert/lib/IEEE754_extra.v#L434
Notation IZR_neq is deprecated since 8.19.
|
|
build (8.18, 64, vst):
compcert/lib/IEEE754_extra.v#L434
Notation IZR_neq is deprecated since 8.19.
|
|
build (8.19, 64, vst):
compcert/lib/IEEE754_extra.v#L434
Notation IZR_neq is deprecated since 8.19.
|
|
build (8.19, 64, vst):
compcert/lib/IEEE754_extra.v#L434
Notation IZR_neq is deprecated since 8.19.
|
|
build (dev, 64, vst):
msl/sepalg.v#L104
Automatically putting Flat_alg in Prop even though it was declared
|
|
build (dev, 64, vst):
msl/sepalg_generators.v#L49
Automatically putting Void in Prop even though it was declared with
|
|
build (dev, 64, vst):
msl/functors.v#L12
Automatically putting functorFacts in Prop even though it was
|
|
build (dev, 64, vst):
msl/functors.v#L30
Automatically putting functorFacts in Prop even though it was
|
|
build (dev, 64, vst):
msl/functors.v#L48
Automatically putting functorFacts in Prop even though it was
|
|
build (dev, 64, vst):
msl/functors.v#L66
Automatically putting functorFacts in Prop even though it was
|
|
build (dev, 64, vst):
msl/functors.v#L87
Automatically putting functorFacts in Prop even though it was
|
|
build (dev, 64, vst):
compcert/lib/Coqlib.v#L861
Notation rev_length is deprecated since 8.20.
|
|
build (dev, 64, vst):
compcert/lib/Coqlib.v#L861
Notation rev_length is deprecated since 8.20.
|
|
build (dev, 64, vst):
compcert/lib/Coqlib.v#L861
Notation rev_length is deprecated since 8.20.
|