Skip to content

Adapt to https://github.com/coq/coq/pull/19530 #625

Adapt to https://github.com/coq/coq/pull/19530

Adapt to https://github.com/coq/coq/pull/19530 #625

Triggered via pull request December 5, 2024 06:58
Status Failure
Total duration 4m 24s
Artifacts

build.yml

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

Annotations

4 errors and 7 warnings
build (dev, 4.09-flambda, local): theories/Type/Constants.v#L40
The reference Corelib.Init.Datatypes.unit was not found in the current
build (dev, 4.09-flambda, hott): theories/HoTT/Classes.v#L11
Cannot find a physical path bound to logical path HoTT.HSet.
build (dev, 4.09-flambda, dune): theories/HoTT/Classes.v#L11
Cannot find a physical path bound to logical path HoTT.HSet.
build (dev, 4.09-flambda, dune): theories/Type/Constants.v#L40
The reference Corelib.Init.Datatypes.unit was not found in the current
build (dev, 4.09-flambda, local)
ubuntu-latest pipelines will use ubuntu-24.04 soon. For more details, see https://github.com/actions/runner-images/issues/10636
build (dev, 4.09-flambda, local): theories/Type/Relation_Properties.v#L40
Notations "_ * _" defined at level 40 with arguments constr
build (dev, 4.09-flambda, hott)
ubuntu-latest pipelines will use ubuntu-24.04 soon. For more details, see https://github.com/actions/runner-images/issues/10636
build (dev, 4.09-flambda, hott): theories/HoTT/Relation_Properties.v#L46
Notations "_ * _" defined at level 40 with arguments constr
build (dev, 4.09-flambda, dune)
ubuntu-latest pipelines will use ubuntu-24.04 soon. For more details, see https://github.com/actions/runner-images/issues/10636
build (dev, 4.09-flambda, dune): theories/Type/Relation_Properties.v#L40
Notations "_ * _" defined at level 40 with arguments constr
build (dev, 4.09-flambda, dune): theories/HoTT/Relation_Properties.v#L46
Notations "_ * _" defined at level 40 with arguments constr