...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`.

1) rely on patch to actually patch the Makefile
2) move ineffective 'sed' hackery related to 'make validate'

Re 2), the sed script didn't actually modify the Makefile anyway
(unlear how long it has been ineffective), so let's just remove it.

Add support for compiling only classic Prosa, i.e., the inverse of
--without-classic.