Add nia tests from Coq test-suite #582
JasonGrossAnnotations
15 errors and 55 warnings
|
build (8.8)
Unable to locate library Zify.
|
|
build (8.9)
Unable to locate library Zify.
|
|
build (8.10)
Unable to locate library Zify.
|
|
build (8.11)
The reference Z.euclidean_division_equations_pose_eq_fact
|
|
build (8.16-native)
The reference Z.euclidean_division_equations_pose_eq_fact
|
|
build (8.12)
The reference Z.euclidean_division_equations_pose_eq_fact
|
|
build (8.19-native)
The reference Z.euclidean_division_equations_pose_eq_fact
|
|
build (8.18-native)
The reference Z.euclidean_division_equations_pose_eq_fact
|
|
build (8.17-native)
The reference Z.euclidean_division_equations_pose_eq_fact
|
|
build (8.13)
The reference Z.euclidean_division_equations_pose_eq_fact
|
|
build (8.14)
The reference Z.euclidean_division_equations_pose_eq_fact
|
|
build (8.15)
The reference Z.euclidean_division_equations_pose_eq_fact
|
|
build (dev-native)
Canceling since a higher priority waiting request for 'CI (Coq)-dev-native-nia' exists
|
|
build (dev-native)
The operation was canceled.
|
|
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.9)
There is no option NativeCompute Timing.
|
|
build (8.9)
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.10)
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.
|
|
build (8.11)
There is no option NativeCompute Timing.
|
|
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.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.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.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.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.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 (dev-native)
Unused variable: id.
|
|
build (dev-native)
Unused variable: id.
|
|
build (dev-native)
Unused variable nlimbs might be a misspelled constructor. Use _ or
|