Add support for Mac #590
Annotations
1 error and 66 warnings
check-all
Process completed with exit code 1.
|
build (8.8)
There is no option NativeCompute Timing.
|
build (8.8)
There is no option NativeCompute Timing.
|
build (8.15)
Unused variable nlimbs catches more than one case.
|
build (8.15)
grammar entry "ident" permitted "_" in addition to proper
|
build (8.15)
grammar entry "ident" permitted "_" in addition to proper
|
build (8.15)
grammar entry "ident" permitted "_" in addition to proper
|
build (8.15)
grammar entry "ident" permitted "_" in addition to proper
|
build (8.15)
native_compute disabled at configure time; falling back to
|
build (8.15)
grammar entry "ident" permitted "_" in addition to proper identifiers; this use is deprecated and its meaning will change in the future; use "name" instead.
|
build (8.15)
grammar entry "ident" permitted "_" in addition to proper identifiers; this use is deprecated and its meaning will change in the future; use "name" instead.
|
build (8.15)
grammar entry "ident" permitted "_" in addition to proper identifiers; this use is deprecated and its meaning will change in the future; use "name" instead.
|
build (8.15)
native_compute disabled at configure time; falling back to vm_compute.
|
build (8.18-native)
Unused variable nlimbs might be a misspelled constructor. Use _ or
|
build (8.19-native)
Unused variable nlimbs might be a misspelled constructor. Use _ or
|
build (8.17-native)
Unused variable nlimbs might be a misspelled constructor. Use _ or
|
build (8.16-native)
Unused variable nlimbs catches more than one case.
|
build (8.14)
Unused variable nlimbs catches more than one case.
|
build (8.14)
grammar entry "ident" permitted "_" in addition to proper
|
build (8.14)
grammar entry "ident" permitted "_" in addition to proper
|
build (8.14)
grammar entry "ident" permitted "_" in addition to proper
|
build (8.14)
grammar entry "ident" permitted "_" in addition to proper
|
build (8.14)
native_compute disabled at configure time; falling back to
|
build (8.14)
grammar entry "ident" permitted "_" in addition to proper identifiers; this use is deprecated and its meaning will change in the future; use "name" instead.
|
build (8.14)
grammar entry "ident" permitted "_" in addition to proper identifiers; this use is deprecated and its meaning will change in the future; use "name" instead.
|
build (8.14)
grammar entry "ident" permitted "_" in addition to proper identifiers; this use is deprecated and its meaning will change in the future; use "name" instead.
|
build (8.14)
native_compute disabled at configure time; falling back to vm_compute.
|
build (8.9)
There is no option NativeCompute Timing.
|
build (8.9)
There is no option NativeCompute Timing.
|
build (dev-native)
Coq.ZArith.ZArith has been replaced by Stdlib.ZArith.ZArith.
|
build (dev-native)
Coq.micromega.Lia has been replaced by Stdlib.micromega.Lia.
|
build (dev-native)
Coq.Classes.Morphisms has been replaced by Stdlib.Classes.Morphisms.
|
build (dev-native)
Coq.Setoids.Setoid has been replaced by Stdlib.Setoids.Setoid.
|
build (dev-native)
Coq.Lists.List has been replaced by Stdlib.Lists.List.
|
build (dev-native)
Coq.Classes.Morphisms has been replaced by Stdlib.Classes.Morphisms.
|
build (dev-native)
Coq.Setoids.Setoid has been replaced by Stdlib.Setoids.Setoid.
|
build (dev-native)
Coq.Classes.Morphisms has been replaced by Stdlib.Classes.Morphisms.
|
build (dev-native)
Coq.Strings.String has been replaced by Stdlib.Strings.String.
|
build (dev-native)
Coq.Structures.Orders has been replaced by Stdlib.Structures.Orders.
|
build (8.10)
There is no option NativeCompute Timing.
|
build (8.10)
There is no option NativeCompute Timing.
|
build (8.10)
There is no option NativeCompute Timing.
|
build (8.10)
There is no option NativeCompute Timing.
|
build (8.10)
There is no option NativeCompute Timing.
|
build (8.10)
There is no option NativeCompute Timing.
|
build (8.10)
There is no option NativeCompute Timing.
|
build (8.10)
There is no option NativeCompute Timing.
|
build (8.10)
There is no option NativeCompute Timing.
|
build (8.13)
Unused variable nlimbs catches more than one case.
|
build (8.13)
grammar entry "ident" permitted "_" in addition to proper
|
build (8.13)
grammar entry "ident" permitted "_" in addition to proper
|
build (8.13)
grammar entry "ident" permitted "_" in addition to proper
|
build (8.13)
grammar entry "ident" permitted "_" in addition to proper
|
build (8.13)
native_compute disabled at configure time; falling back to
|
build (8.13)
grammar entry "ident" permitted "_" in addition to proper identifiers; this use is deprecated and its meaning will change in the future; use "name" instead.
|
build (8.13)
grammar entry "ident" permitted "_" in addition to proper identifiers; this use is deprecated and its meaning will change in the future; use "name" instead.
|
build (8.13)
grammar entry "ident" permitted "_" in addition to proper identifiers; this use is deprecated and its meaning will change in the future; use "name" instead.
|
build (8.13)
native_compute disabled at configure time; falling back to vm_compute.
|
build (8.11)
There is no option NativeCompute Timing.
|
build (8.11)
There is no option NativeCompute Timing.
|
build (8.11)
There is no option NativeCompute Timing.
|
build (8.11)
There is no option NativeCompute Timing.
|
build (8.11)
There is no option NativeCompute Timing.
|
build (8.11)
There is no option NativeCompute Timing.
|
build (8.11)
There is no option NativeCompute Timing.
|
build (8.11)
There is no option NativeCompute Timing.
|
build (8.11)
There is no option NativeCompute Timing.
|