Provide a convenience hypothesis with eqv assumptions in rewrite rules side-conditions #568
JasonGrossdocker-coq.yml
on: pull_request
Matrix: build-docker
check-all-docker
0s
Annotations
20 warnings
|
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.
|
|
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/plugins/Ltac2Extra.v#L9
Trying to mask the absolute name "Ltac2.Constr"!
|
|
build-docker (8.16):
src/Rewriter/Util/plugins/Ltac2Extra.v#L10
Trying to mask the absolute name "Ltac2.Constr"!
|
|
build-docker (8.16):
src/Rewriter/Language/Reify.v#L67
Trying to mask the absolute name "Ltac2.Ident"!
|
|
build-docker (8.16):
src/Rewriter/Language/Reify.v#L68
Trying to mask the absolute name "Ltac2.Ident"!
|
|
build-docker (8.16):
src/Rewriter/Language/Reify.v#L310
Ltac2 definition Ltac1.get_to_constr is deprecated since 8.15.
Use Ltac2 instead.
|