Skip to content

Fix breakage from https://github.com/coq/coq/pull/18374 #2562

Fix breakage from https://github.com/coq/coq/pull/18374

Fix breakage from https://github.com/coq/coq/pull/18374 #2562

Triggered via pull request December 8, 2023 16:27
Status Failure
Total duration 11m 27s
Artifacts

build.yml

on: pull_request
checktodos
3s
checktodos
Matrix: build
Fit to window
Zoom out
Zoom in

Annotations

7 errors and 30 warnings
build (dev, 4.14-flambda, quick)
Universe instance length is 2 but should be 3.
build (dev, 4.14-flambda, local)
The job was canceled because "dev_4_14-flambda_quick" failed.
build (dev, 4.14-flambda, local)
Cannot find a physical path bound to logical path Even.
build (dev, 4.14-flambda, local)
The operation was canceled.
build (dev, 4.14-flambda, opam)
The job was canceled because "dev_4_14-flambda_quick" failed.
build (dev, 4.14-flambda, opam)
Cannot find a physical path bound to logical path Even.
build (dev, 4.14-flambda, opam)
The operation was canceled.
build (dev, 4.14-flambda, quick)
The '%' scope delimiter in 'Arguments' commands is deprecated, use
build (dev, 4.14-flambda, quick)
Tactic Notation revert dependent (hyp) is deprecated since 8.18.
build (dev, 4.14-flambda, quick)
Tactic Notation revert dependent (hyp) is deprecated since 8.18.
build (dev, 4.14-flambda, quick)
The '%' scope delimiter in 'Arguments' commands is deprecated, use
build (dev, 4.14-flambda, quick)
The '%' scope delimiter in 'Arguments' commands is deprecated, use
build (dev, 4.14-flambda, quick)
The '%' scope delimiter in 'Arguments' commands is deprecated, use
build (dev, 4.14-flambda, quick)
Notation "_ =1 _" was already used in scope type_scope.
build (dev, 4.14-flambda, quick)
Notation "_ =2 _" was already used in scope type_scope.
build (dev, 4.14-flambda, quick)
Overwriting previous delimiting key B in scope bool_scope
build (dev, 4.14-flambda, quick)
Notation "_ =1 _" was already used in scope type_scope.
build (dev, 4.14-flambda, local)
The '%' scope delimiter in 'Arguments' commands is deprecated, use
build (dev, 4.14-flambda, local)
Tactic Notation revert dependent (hyp) is deprecated since 8.18.
build (dev, 4.14-flambda, local)
Tactic Notation revert dependent (hyp) is deprecated since 8.18.
build (dev, 4.14-flambda, local)
The '%' scope delimiter in 'Arguments' commands is deprecated, use
build (dev, 4.14-flambda, local)
The '%' scope delimiter in 'Arguments' commands is deprecated, use
build (dev, 4.14-flambda, local)
The '%' scope delimiter in 'Arguments' commands is deprecated, use
build (dev, 4.14-flambda, local)
Notation "_ =1 _" was already used in scope type_scope.
build (dev, 4.14-flambda, local)
Notation "_ =2 _" was already used in scope type_scope.
build (dev, 4.14-flambda, local)
Overwriting previous delimiting key B in scope bool_scope
build (dev, 4.14-flambda, local)
Notation "_ =1 _" was already used in scope type_scope.
build (dev, 4.14-flambda, opam)
The '%' scope delimiter in 'Arguments' commands is deprecated, use
build (dev, 4.14-flambda, opam)
Tactic Notation revert dependent (hyp) is deprecated since 8.18.
build (dev, 4.14-flambda, opam)
Tactic Notation revert dependent (hyp) is deprecated since 8.18.
build (dev, 4.14-flambda, opam)
The '%' scope delimiter in 'Arguments' commands is deprecated, use
build (dev, 4.14-flambda, opam)
Tactic Notation revert dependent (hyp) is deprecated since 8.18.
build (dev, 4.14-flambda, opam)
Tactic Notation revert dependent (hyp) is deprecated since 8.18.
build (dev, 4.14-flambda, opam)
The '%' scope delimiter in 'Arguments' commands is deprecated, use
build (dev, 4.14-flambda, opam)
The '%' scope delimiter in 'Arguments' commands is deprecated, use
build (dev, 4.14-flambda, opam)
The '%' scope delimiter in 'Arguments' commands is deprecated, use
build (dev, 4.14-flambda, opam)
Notation "_ =1 _" was already used in scope type_scope.