Skip to content

clean up priority-related facts

Björn Brandenburg requested to merge wip-prio-cleanup into master
  • avoid unfolding coercions all over the place
  • reduce unfolding of priority policies
  • provide hep_job and hep_job_at rewriting lemmas
  • shorten some generality proofs

Merge request reports