Sergey Bozhko authored 3 years ago and Björn Brandenburg committed 3 years ago

From changelog of Coq version 8.15:
Changed: [apply with] does not rename arguments unless using
compatibility flag Apply With Renaming (#13837, fixes #13759, by Gaëtan
Gilbert).

So, this commit replaces all occurrences of [apply L with (NAME0 := V)]
to [apply L with (NAME := V)]

Sergey Bozhko authored 3 years ago and Björn Brandenburg committed 3 years ago

* rename [step_function] to [unit_growth]
* restructure file

Mariam Vardishvili authored 3 years ago and Björn Brandenburg committed 3 years ago

The lemma [instantiated_busy_interval_equivalent_edf_busy_interval] actually does not depend on EDF.

lemma [count_filter_fun] is equivalent to ssreflect's [size_filter]

Sergey Bozhko authored 3 years ago and Björn Brandenburg committed 3 years ago

Note that many files have changed; however, this is due to the fact that some of the lemmas in nat.v have been renamed or removed.

Can't rely on arg_maxnP just yet.

This change breaks compatibility with mathcomp < 1.10.

There's now also a `findP` in ssreflect's seq library.

Vedant Chavda authored 4 years ago and Björn Brandenburg committed 4 years ago

change it to perm_big

Move everything into the new namespace starting with 'prosa' rather
than the bland 'rt'.

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.