The vernacular commands Opaque / Transparent change coqtop's prompt
counter without generating a prompt (for whatever reason). The proof
state recorder needs to be aware of this to avoid a out-of-sync
assertion false positive.

For debugging purposes, slow down the interaction with coqtop to maybe
trigger some potential races more reliably.

If coqtop reports a different number of interactions in its prompt
than we provided, we're out of sync.

... to comments and closing braces on lines before bulleted
sub-proofs.

For better debugging support, add

	--parse-only
and

	--parse-only --verbose
modes.

So that we can link them to arrival curves of Network Calculus
in NCCoq.

Don't always "drill to the bottom" and unfold to sums; instead
explicitly make use of the fact that the EDF proof reasons about
finite identical prefixes, which allows staying at a semantically
higher level in the proof.

While at it, switch the file to using the preferred `now` tactical
when closing out proofs (rather than `by`) to avoid emacs indentation
issues.

Before mathcomp 1.11.0 (which requires Coq 8.12), case analysis
doesn't automatically rewrite destructed `minn` premises, so "try"
this manually until we drop support for mathcomp 1.11.0.

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.

add lemmas on consistency of backlogged jobs set

add notion of a non-clairvoyant readiness model

This is a general definition and not specific to a particular
implementation.