Bump etc/coq-scripts from 8b66ebe
to 2df5dbe
#149
docker-coq.yml
on: pull_request
Matrix: build
check-all-docker
2s
Annotations
41 warnings
8.17 (fiat-core parsers):
src/Common/Coq__8_4__8_5__Compat.v#L11
There is no flag or option with this name: "Template Check".
|
8.17 (fiat-core parsers):
src/Common/Coq__8_4__8_5__Compat.v#L29
There is no flag or option with this name:
|
8.17 (fiat-core parsers):
src/Parsers/StringLike/Core.v#L21
A coercion will be introduced instead of an instance in future
|
8.17 (fiat-core parsers):
src/Parsers/StringLike/Core.v#L47
Declaring a scope implicitly is deprecated; use in advance an
|
8.17 (fiat-core parsers):
src/Parsers/StringLike/Core.v#L107
A coercion will be introduced instead of an instance in future
|
8.17 (fiat-core parsers):
src/Computation/Decidable.v#L153
Notation beq_nat is deprecated since 8.16. Use Nat.eqb instead.
|
8.17 (fiat-core parsers):
src/Computation/Decidable.v#L155
Notation beq_nat_true_iff is deprecated since 8.16.
|
8.17 (fiat-core parsers):
src/Computation/Decidable.v#L155
Notation beq_nat_true_iff is deprecated since 8.16.
|
8.17 (fiat-core parsers):
src/Parsers/ExtrOcamlPrimitives.v#L17
Declaring a scope implicitly is deprecated; use in advance an
|
8.17 (fiat-core parsers):
src/Computation/Notations.v#L20
Declaring a scope implicitly is deprecated; use in advance an
|
8.16 (fiat-core parsers):
src/Common/Coq__8_4__8_5__Compat.v#L11
There is no flag or option with this name: "Template Check".
|
8.16 (fiat-core parsers):
src/Common/Coq__8_4__8_5__Compat.v#L29
There is no flag or option with this name:
|
8.16 (fiat-core parsers):
src/Parsers/StringLike/Core.v#L47
Declaring a scope implicitly is deprecated; use in advance an
|
8.16 (fiat-core parsers):
src/Computation/Decidable.v#L153
Notation beq_nat is deprecated since 8.16. Use Nat.eqb instead.
|
8.16 (fiat-core parsers):
src/Computation/Decidable.v#L155
Notation beq_nat_true_iff is deprecated since 8.16.
|
8.16 (fiat-core parsers):
src/Computation/Decidable.v#L155
Notation beq_nat_true_iff is deprecated since 8.16.
|
8.16 (fiat-core parsers):
src/Parsers/ExtrOcamlPrimitives.v#L17
Declaring a scope implicitly is deprecated; use in advance an
|
8.16 (fiat-core parsers):
src/Computation/Notations.v#L20
Declaring a scope implicitly is deprecated; use in advance an
|
8.16 (fiat-core parsers):
src/Common/BoolFacts.v#L11
Declaring a scope implicitly is deprecated; use in advance an
|
8.16 (fiat-core parsers):
src/Common/Frame.v#L215
Notation Le.le_refl is deprecated since 8.16.
|
8.18 (fiat-core parsers):
src/Common/Coq__8_4__8_5__Compat.v#L11
There is no flag or option with this name: "Template Check".
|
8.18 (fiat-core parsers):
src/Common/Coq__8_4__8_5__Compat.v#L29
There is no flag or option with this name:
|
8.18 (fiat-core parsers):
src/Common/Coq__8_4__8_5__Compat.v#L30
There is no flag or option with this name: "Apply With Renaming".
|
8.18 (fiat-core parsers):
src/Common/Tactics/PrintContext.v#L1
Trying to mask the absolute name "Coq.Lists.ListSet"!
|
8.18 (fiat-core parsers):
src/Common/Tactics/PrintContext.v#L1
Trying to mask the absolute name "Coq.Lists.ListSet"!
|
8.18 (fiat-core parsers):
src/Common/Tactics/PrintContext.v#L1
Trying to mask the absolute name "Coq.Lists.ListSet.set_diff_nodup"!
|
8.18 (fiat-core parsers):
src/Common/Tactics/IsClosed.v#L1
Trying to mask the absolute name "Coq.Lists.ListSet"!
|
8.18 (fiat-core parsers):
src/Common/Tactics/IsClosed.v#L1
Trying to mask the absolute name "Coq.Lists.ListSet"!
|
8.18 (fiat-core parsers):
src/Common/Tactics/IsClosed.v#L1
Trying to mask the absolute name "Coq.Lists.ListSet.set_diff_nodup"!
|
8.18 (fiat-core parsers):
src/Parsers/StringLike/Core.v#L5
Trying to mask the absolute name "Coq.Lists.ListSet"!
|
dev (fiat-core parsers):
src/Common/Coq__8_4__8_5__Compat.v#L11
There is no flag or option with this name: "Template Check".
|
dev (fiat-core parsers):
src/Common/Coq__8_4__8_5__Compat.v#L27
There is no flag or option with this name:
|
dev (fiat-core parsers):
src/Common/Coq__8_4__8_5__Compat.v#L28
There is no flag or option with this name: "Apply With Renaming".
|
dev (fiat-core parsers):
src/Common/Coq__8_4__8_5__Compat.v#L56
Use of “Require” inside a module is fragile. It is not recommended
|
dev (fiat-core parsers):
src/Common/Coq__8_4__8_5__Compat.v#L57
Use of “Require” inside a module is fragile. It is not recommended
|
dev (fiat-core parsers):
src/Common/Coq__8_4__8_5__Compat.v#L58
Use of “Require” inside a module is fragile. It is not recommended
|
dev (fiat-core parsers):
src/Common/Coq__8_4__8_5__Compat.v#L59
Use of “Require” inside a module is fragile. It is not recommended
|
dev (fiat-core parsers):
src/Common/Tactics/Combinators.v#L1
Trying to mask the absolute name "Coq.Lists.ListSet"!
|
dev (fiat-core parsers):
src/Common/Tactics/Combinators.v#L1
Trying to mask the absolute name "Coq.Lists.ListSet"!
|
dev (fiat-core parsers):
src/Common/Tactics/Combinators.v#L1
Trying to mask the absolute name "Coq.Lists.ListSet.set_diff_nodup"!
|
dev (fiat-core parsers)
Docker build failed with exit code 1, back off 1.143 seconds before retry.
|