Adapt to Coq/Coq#18164 #528
JasonGross
This run and associated checks have been archived and are scheduled for deletion.
Learn more about checks retention
docker-coq.yml
on: pull_request
Matrix: build-docker
check-all-docker
1s
Annotations
20 warnings
|
build-docker (8.16):
src/Rewriter/Util/NatUtil.v#L445
Notation le_plus_minus_r is deprecated since 8.16.
The Arith.Minus file is obsolete. Use Nat.sub_add (together with Nat.add_comm) instead.
|
|
build-docker (8.16):
src/Rewriter/Util/NatUtil.v#L445
Notation le_plus_minus_r is deprecated since 8.16.
The Arith.Minus file is obsolete. Use Nat.sub_add (together with Nat.add_comm) instead.
|
|
build-docker (8.16):
src/Rewriter/Util/NatUtil.v#L445
Notation le_plus_minus_r is deprecated since 8.16.
The Arith.Minus file is obsolete. Use Nat.sub_add (together with Nat.add_comm) instead.
|
|
build-docker (8.16):
src/Rewriter/Util/Tactics2/Ltac1.v#L15
Ltac2 definition get_to_constr is deprecated since 8.15.
Use Ltac2 instead.
|
|
build-docker (8.16):
src/Rewriter/Rewriter/Examples/PerfTesting/Sample.v#L749
native_compute disabled at configure time; falling back to
vm_compute.
|
|
build-docker (8.16):
src/Rewriter/Util/Strings/String.v#L120
Notation Minus.minus_n_O is deprecated since 8.16.
The Arith.Minus file is obsolete. Use Nat.sub_0_r (and symmetry of equality) instead.
|
|
build-docker (8.16):
src/Rewriter/Util/Strings/String.v#L120
Notation Minus.minus_n_O is deprecated since 8.16.
The Arith.Minus file is obsolete. Use Nat.sub_0_r (and symmetry of equality) instead.
|
|
build-docker (8.16):
src/Rewriter/Util/Strings/String.v#L120
Notation Minus.minus_n_O is deprecated since 8.16.
The Arith.Minus file is obsolete. Use Nat.sub_0_r (and symmetry of equality) instead.
|
|
build-docker (8.16):
src/Rewriter/Util/Strings/String.v#L120
Notation Minus.minus_n_O is deprecated since 8.16.
The Arith.Minus file is obsolete. Use Nat.sub_0_r (and symmetry of equality) instead.
|
|
build-docker (8.16):
src/Rewriter/Util/Strings/String.v#L120
Notation Minus.minus_n_O is deprecated since 8.16.
The Arith.Minus file is obsolete. Use Nat.sub_0_r (and symmetry of equality) instead.
|
|
build-docker (dev)
Could not find a terminator for warning:
File "./src/Rewriter/Util/NatUtil.v", line 53, characters 35-42:
Warning: Notation mod_mod is deprecated since 8.17. Use Div0.mod_mod instead.
[deprecated-syntactic-definition-since-8.17,deprecated-since-8.17,deprecated-syntactic-definition,deprecated,default]
|
|
build-docker (dev):
src/Rewriter/Util/NatUtil.v#L53
Notation mod_mod is deprecated since 8.17. Use Div0.mod_mod instead.
|
|
build-docker (dev)
Could not find a terminator for warning:
File "./src/Rewriter/Util/NatUtil.v", line 192, characters 43-50:
Warning: Notation mod_add is deprecated since 8.17. Use Div0.mod_add instead.
[deprecated-syntactic-definition-since-8.17,deprecated-since-8.17,deprecated-syntactic-definition,deprecated,default]
|
|
build-docker (dev):
src/Rewriter/Util/NatUtil.v#L192
Notation mod_add is deprecated since 8.17. Use Div0.mod_add instead.
|
|
build-docker (dev)
Could not find a terminator for warning:
File "./src/Rewriter/Util/NatUtil.v", line 192, characters 43-50:
Warning: Notation mod_add is deprecated since 8.17. Use Div0.mod_add instead.
[deprecated-syntactic-definition-since-8.17,deprecated-since-8.17,deprecated-syntactic-definition,deprecated,default]
|
|
build-docker (dev):
src/Rewriter/Util/NatUtil.v#L192
Notation mod_add is deprecated since 8.17. Use Div0.mod_add instead.
|
|
build-docker (dev)
Could not find a terminator for warning:
File "./src/Rewriter/Util/NatUtil.v", line 221, characters 12-23:
Warning: Notation mod_add is deprecated since 8.17. Use Div0.mod_add instead.
[deprecated-syntactic-definition-since-8.17,deprecated-since-8.17,deprecated-syntactic-definition,deprecated,default]
|
|
build-docker (dev):
src/Rewriter/Util/NatUtil.v#L221
Notation mod_add is deprecated since 8.17. Use Div0.mod_add instead.
|
|
build-docker (dev)
Could not find a terminator for warning:
File "./src/Rewriter/Util/NatUtil.v", line 221, characters 12-23:
Warning: Notation mod_add is deprecated since 8.17. Use Div0.mod_add instead.
[deprecated-syntactic-definition-since-8.17,deprecated-since-8.17,deprecated-syntactic-definition,deprecated,default]
|
|
build-docker (dev):
src/Rewriter/Util/NatUtil.v#L221
Notation mod_add is deprecated since 8.17. Use Div0.mod_add instead.
|