Remove unused Require Even (Even has been removed from stdlib in 8.19) #2592
SkySkimmerAnnotations
5 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)
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)
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.
|