Skip to content

Bump etc/coq-scripts from 2df5dbe to d3dc888 #535

Bump etc/coq-scripts from 2df5dbe to d3dc888

Bump etc/coq-scripts from 2df5dbe to d3dc888 #535

Triggered via push November 7, 2023 15:37
Status Success
Total duration 58m 41s
Artifacts

docker-coq.yml

on: push
Matrix: build-docker
check-all-docker
0s
check-all-docker
Fit to window
Zoom out
Zoom in

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.