tweak proofs to be less "bulky" and less brittle

Status Job ID Name Coverage
  Build
passed #50315
1.9.0-coq-8.10

00:01:46

passed #50316
1.9.0-coq-8.10-classic

00:02:54

passed #50319
1.9.0-coq-8.9

00:01:44

failed #50320
allowed to fail
1.9.0-coq-dev

00:01:11

passed #50321
allowed to fail
latest-coq-8.10

00:01:46

passed #50317
proof-length

00:00:27

failed #50318
spell-check

00:00:32

 
  Process
passed #50324
doc

00:00:23

passed #50325
doc-classic

00:00:28

failed #50326
proof-state

00:01:10

passed #50322
validate

00:00:50

passed #50323
validate-classic

00:00:53

 
Name Stage Failure
failed
proof-state Process
Collecting proof state for util/all.v...
Collecting proof state for util/div_mod.v...
Collecting proof state for util/epsilon.v...
Collecting proof state for util/ssromega.v...
Collecting proof state for util/search_arg.v...
Collecting proof state for util/rewrite_facilities.v...
Collecting proof state for util/sum.v...
Collecting proof state for util/nat.v...
ERROR: Job failed: exit code 1
failed
1.9.0-coq-dev Build
COQC restructuring/analysis/facts/preemption/task/floating.v
COQC restructuring/analysis/transform/prefix.v
File "./restructuring/analysis/facts/preemption/task/floating.v", line 69, characters 8-87:
Error: No applicable tactic.

make[1]: *** [Makefile:679: restructuring/analysis/facts/preemption/task/floating.vo] Error 1
make[1]: *** Waiting for unfinished jobs....
make: *** [Makefile:327: all] Error 2
ERROR: Job failed: exit code 1
failed
spell-check Build
./restructuring/analysis/transform/facts/wc_correctness.v: potentially misspelled word 'arg'
./restructuring/analysis/transform/facts/wc_correctness.v: potentially misspelled word 'ication'
./restructuring/analysis/transform/facts/wc_correctness.v: potentially misspelled word 'pstate'
./restructuring/analysis/transform/facts/wc_correctness.v: potentially misspelled word 'sched'
./restructuring/analysis/transform/facts/wc_correctness.v: potentially misspelled word 'wc'
./restructuring/analysis/transform/facts/wc_correctness.v: potentially misspelled word 'xpred'
./restructuring/analysis/transform/wc_trans.v: potentially misspelled word 'ification'
./restructuring/analysis/transform/wc_trans.v: potentially misspelled word 'wc'
ERROR: Job failed: exit code 1