Coq 8.20, rm infra.v, minor fixes · math-comp/trajectories@46e028f

Triggered via pull request February 19, 2025 14:25

synchronize #38

fix_20250219

Status Failure

Total duration 22m 22s

Artifacts –

docker-action.yml

on: pull_request

Matrix: build

1 error and 10 warnings

The reference Order.TMeetTheory.meets_ge was not found in the current

Ignoring canonical projection to GRing.scalable_linear by

Ignoring canonical projection to pair_of_and by

Ignoring canonical projection to GRing.scalable_linear by

Ignoring canonical projection to pair_of_and by

Ignoring canonical projection to GRing.scalable_linear by

Ignoring canonical projection to pair_of_and by

Notation rolle is deprecated since mathcomp-real-closed 2.1.0.

Notation rolle is deprecated since mathcomp-real-closed 2.1.0.

Ignoring canonical projection to GRing.scalable_linear by

Ignoring canonical projection to pair_of_and by