Skip to content

CI: automatically check validation output for unexpected axioms

Björn Brandenburg requested to merge axiom-check into master

Extend the check in CI to ensure that we don't accidentally start depending on any unwanted axioms.

Contains a workaround for Coq issue 13324, which currently results in some bogus axioms being listed. Once upstream Coq has been fixed, this workaround should be removed, but it's unlikely to falsify the results even if it remains in place.

Closes #79 (closed).

Merge request reports