Co-authored-by: Björn Brandenburg <bbb@mpi-sws.org>

Athul Raj Kollareth authored 1 month ago and Björn Brandenburg committed 1 month ago

... for all four preemption models. 

This definition isn't actually used anywhere important, maybe it's
time to get rid of it.

Athul Raj Kollareth authored 3 months ago and Björn Brandenburg committed 1 month ago

Co-authored-by: Kimaya Bedarkar <kbedarka@mpi-sws.org>
Co-authored-by: Björn Brandenburg <bbb@mpi-sws.org>

Co-authored-by: Sergey Bozhko <sbozhko@mpi-sws.org>

Since `coqchk` is not precise, we keep running into false positives
when packages that we (indirectly) depend on (in particular,`coq-elpi`)
load the standard library. Currently, this blocks the upgrade to Coq 8.20.

This patch disables `make validate` and instead introduces a check
that runs `Print Assumptions` for each theorem in the `prosa.results`
module, which are all the main results we care about.