Skip to content
CI (Coq, docker, dev)

Adapt to coq/coq#17475 (Ltac2 externals can have arity 0) #462

Sign in to view logs

Adapt to coq/coq#17475 (Ltac2 externals can have arity 0)

Adapt to coq/coq#17475 (Ltac2 externals can have arity 0) #462

Triggered via pull request April 28, 2023 11:48
@SkySkimmerSkySkimmer
opened #102
SkySkimmer:ltac2-defineval
Status Failure
Total duration 1m 21s
Artifacts –

docker-coq.yml

on: pull_request
build-dev
1m 13s
build-dev
Fit to window
Zoom out
Zoom in

Annotations

10 warnings
build-dev: src/Rewriter/Util/NatUtil.v#L53
Notation plus_le_compat is deprecated since 8.16. The Arith.Plus file is obsolete. Use Nat.add_le_mono instead.
build-dev: src/Rewriter/Util/NatUtil.v#L54
Notation mod_mod is deprecated since 8.17. Use Div0.mod_mod instead.
build-dev: src/Rewriter/Util/NatUtil.v#L71
Notation Min.min_case_strong is deprecated since 8.16. The Arith.Min file is obsolete. Use Nat.min_case_strong instead.
build-dev: src/Rewriter/Util/NatUtil.v#L71
Notation Min.min_case_strong is deprecated since 8.16. The Arith.Min file is obsolete. Use Nat.min_case_strong instead.
build-dev: src/Rewriter/Util/NatUtil.v#L73
Notation Max.max_case_strong is deprecated since 8.16. The Arith.Max file is obsolete. Use Nat.max_case_strong instead.
build-dev: src/Rewriter/Util/NatUtil.v#L73
Notation Max.max_case_strong is deprecated since 8.16. The Arith.Max file is obsolete. Use Nat.max_case_strong instead.
build-dev: src/Rewriter/Util/NatUtil.v#L87
Notation Max.max_case_strong is deprecated since 8.16. The Arith.Max file is obsolete. Use Nat.max_case_strong instead.
build-dev: src/Rewriter/Util/NatUtil.v#L86
Notation Min.min_case_strong is deprecated since 8.16. The Arith.Min file is obsolete. Use Nat.min_case_strong instead.
build-dev: src/Rewriter/Util/NatUtil.v#L193
Notation mod_add is deprecated since 8.17. Use Div0.mod_add instead.
build-dev: src/Rewriter/Util/NatUtil.v#L193
Notation mod_add is deprecated since 8.17. Use Div0.mod_add instead.