Skip to content
Snippets Groups Projects
Commit b9f30084 authored by Björn Brandenburg's avatar Björn Brandenburg
Browse files

CI: replace `make validate` with `Print Assumptions`

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.
parent 9a59a1fb
No related branches found
No related tags found
Loading
Checking pipeline status