Skip to content

Coq 8.20, rm infra.v, minor fixes #147

Coq 8.20, rm infra.v, minor fixes

Coq 8.20, rm infra.v, minor fixes #147

Triggered via pull request February 19, 2025 11:25
Status Failure
Total duration 20m 50s
Artifacts

docker-action.yml

on: pull_request
Matrix: build
Fit to window
Zoom out
Zoom in

Annotations

1 error
build (mathcomp/mathcomp:2.2.0-coq-8.19): theories/preliminaries.v#L184
The reference Order.disp_t was not found in the current environment.