Related issue: #37

Now that we have non-ambiguous dependencies, parallel builds should
work without issue.

This fixes all warnings about ambiguous module names and resolves #49.

It also highlights that we still need to cut down on superfluous
Require Import commands in recently ported files.

...and "Defined" can end one.

This can be useful for learning / teaching.

Add instantiations of aRTA for
(1) fully preemptive,
(2) fully non-preemptive,
(3) limited preemptions,
(4) and floating non-preemptive regions EDF models

Add instantiations of aRTA for
(1) fully preemptive,
(2) fully non-preemptive,
(3) limited preemptions,
(4) and floating non-preemptive regions FP models

File preemption.util is renamed and moved to
util.nondecreasing. The new util file can be used
in both the old Prosa and the new Prosa.

Use coqdoc's header feature to make it easier to find key concepts and
improve/tweak a few comments.

Marco Perronet authored 5 years ago and Björn Brandenburg committed 5 years ago

... to get support for proofs started by `Next Obligation`.