Merge github.com:AbsInt/CompCert into kvx-work

11 jobs for kvx-work in 254 minutes and 18 seconds (queued for 13 minutes and 1 second)
Status Job ID Name Coverage
  Build
failed #183095
build_aarch64

00:11:32

passed #183096
build_arm

02:21:02

passed #183097
build_armhf

02:27:09

passed #183094
build_ia32

02:06:51

passed #183102
build_kvx

01:34:16

failed #183098
build_ppc

00:04:47

failed #183099
build_ppc64

00:04:37

passed #183101
build_rv32

00:13:33

passed #183100
build_rv64

00:39:17

passed #183093
build_x86_64

00:49:13

passed #183092
check-admitted

00:01:25

 
Name Stage Failure
failed
build_ppc64 Build
Error: The components of this disjunctive pattern must bind the same
variables (Ointuoffloat is not bound in all patterns).

make[1]: *** [Makefile:273: powerpc/Op.vo] Error 1
make[1]: *** Waiting for unfinished jobs....
make[1]: Leaving directory '/builds/certicompil/compcert-kvx'
make: *** [Makefile:190: all] Error 2
Cleaning up file based variables
ERROR: Job failed: exit code 1
failed
build_ppc Build
Error: The components of this disjunctive pattern must bind the same
variables (Ointuoffloat is not bound in all patterns).

make[1]: *** [Makefile:273: powerpc/Op.vo] Error 1
make[1]: *** Waiting for unfinished jobs....
make[1]: Leaving directory '/builds/certicompil/compcert-kvx'
make: *** [Makefile:190: all] Error 2
Cleaning up file based variables
ERROR: Job failed: exit code 1
failed
build_aarch64 Build
COQC aarch64/Asmgenproof.v
File "./aarch64/Asmgenproof.v", line 888, characters 2-20:
Error: Found no subterm matching "In ?y0 (map ?y ?l)" in the current goal.

make[1]: *** [Makefile:273: aarch64/Asmgenproof.vo] Error 1
make[1]: Leaving directory '/builds/certicompil/compcert-kvx'
make: *** [Makefile:190: all] Error 2
Cleaning up file based variables
ERROR: Job failed: exit code 1