Update main_theorem.v

6 jobs for martin in 23 seconds (queued for 2 seconds)
Status Job ID Name Coverage
  Build
failed #39733
1.8.0-coq-8.8

00:00:22

failed #39735
1.9.0-coq-8.9

00:00:22

failed #39734
allowed to fail
1.9.0-coq-dev

00:00:14

 
  Process
skipped #39737
doc
skipped #39738
proof-length
skipped #39736
validate
 
Name Stage Failure
failed
1.9.0-coq-8.9 Build There is an unknown failure, please try again

make[1]: *** [Makefile:663: restructuring/analysis/fpp_implicit_deadline/workload_bound_fp.vo] Error 1
make[1]: *** Waiting for unfinished jobs....
File "./restructuring/analysis/fpp_implicit_deadline/intermediate.v", line 559, characters 14-26:
Error: The reference arithmetic_1 was not found in the current environment.

make[1]: *** [Makefile:663: restructuring/analysis/fpp_implicit_deadline/intermediate.vo] Error 1
make: *** [Makefile:327: all] Error 2
ERROR: Job failed: exit code 1
failed
1.8.0-coq-8.8 Build There is an unknown failure, please try again

make[1]: *** [Makefile:657: restructuring/analysis/fpp_implicit_deadline/workload_bound_fp.vo] Error 1
make[1]: *** Waiting for unfinished jobs....
File "./restructuring/analysis/fpp_implicit_deadline/intermediate.v", line 559, characters 14-26:
Error: The reference arithmetic_1 was not found in the current environment.

make[1]: *** [Makefile:657: restructuring/analysis/fpp_implicit_deadline/intermediate.vo] Error 1
make: *** [Makefile:318: all] Error 2
ERROR: Job failed: exit code 1
failed
1.9.0-coq-dev Build There is an unknown failure, please try again
COQC util/powerset.v
COQC util/seqset.v
File "./util/seqset.v", line 19, characters 42-52:
Error: The reference mkPredType was not found in the current environment.

make[1]: *** [Makefile:659: util/seqset.vo] Error 1
make[1]: *** Waiting for unfinished jobs....
make: *** [Makefile:321: all] Error 2
ERROR: Job failed: exit code 1