Skip to content
CI (Coq, docker)

Adapt to https://github.com/coq/coq/pull/19530 #233

Sign in to view logs

Adapt to https://github.com/coq/coq/pull/19530

Adapt to https://github.com/coq/coq/pull/19530 #233

Triggered via pull request September 17, 2024 07:06
@JasonGrossJasonGross
synchronize #113
proux01:stdlib_repo
Status Success
Total duration 6m 49s
Artifacts –

coq.yml

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

Annotations

60 warnings
dev (fiat-core parsers parsers-examples coq-ci): src/Common/Coq__8_4__8_5__Compat.v#L12
There is no flag or option with this name: "Template Check".
dev (fiat-core parsers parsers-examples coq-ci): src/Common/Coq__8_4__8_5__Compat.v#L28
There is no flag or option with this name:
dev (fiat-core parsers parsers-examples coq-ci): src/Common/Coq__8_4__8_5__Compat.v#L29
There is no flag or option with this name: "Apply With Renaming".
dev (fiat-core parsers parsers-examples coq-ci): 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 parsers-examples coq-ci): 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 parsers-examples coq-ci): 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 parsers-examples coq-ci): src/Common/Coq__8_4__8_5__Compat.v#L60
Use of “Require” inside a module is fragile. It is not recommended
dev (fiat-core parsers parsers-examples coq-ci): src/Common/Coq__8_4__8_5__Compat.v#L610
Using Vector.t is known to be technically difficult, see
dev (fiat-core parsers parsers-examples coq-ci): src/Computation/Notations.v#L6
Closed notations (i.e. starting and ending with a terminal symbol)
dev (fiat-core parsers parsers-examples coq-ci): src/Computation/Notations.v#L20
Declaring a scope implicitly is deprecated; use in advance an
8.20 (fiat-core parsers parsers-examples coq-ci): src/Common/Coq__8_4__8_5__Compat.v#L12
There is no flag or option with this name: "Template Check".
8.20 (fiat-core parsers parsers-examples coq-ci): src/Common/Coq__8_4__8_5__Compat.v#L28
There is no flag or option with this name:
8.20 (fiat-core parsers parsers-examples coq-ci): src/Common/Coq__8_4__8_5__Compat.v#L29
There is no flag or option with this name: "Apply With Renaming".
8.20 (fiat-core parsers parsers-examples coq-ci): src/Common/Coq__8_4__8_5__Compat.v#L57
Use of “Require” inside a module is fragile. It is not recommended
8.20 (fiat-core parsers parsers-examples coq-ci): src/Common/Coq__8_4__8_5__Compat.v#L58
Use of “Require” inside a module is fragile. It is not recommended
8.20 (fiat-core parsers parsers-examples coq-ci): src/Common/Coq__8_4__8_5__Compat.v#L59
Use of “Require” inside a module is fragile. It is not recommended
8.20 (fiat-core parsers parsers-examples coq-ci): src/Common/Coq__8_4__8_5__Compat.v#L60
Use of “Require” inside a module is fragile. It is not recommended
8.20 (fiat-core parsers parsers-examples coq-ci): src/Common/Coq__8_4__8_5__Compat.v#L610
Using Vector.t is known to be technically difficult, see
8.20 (fiat-core parsers parsers-examples coq-ci): src/Computation/Notations.v#L6
Closed notations (i.e. starting and ending with a terminal symbol)
8.20 (fiat-core parsers parsers-examples coq-ci): src/Computation/Notations.v#L20
Declaring a scope implicitly is deprecated; use in advance an
8.18 (fiat-core parsers parsers-examples coq-ci): 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 parsers-examples coq-ci): src/Common/Coq__8_4__8_5__Compat.v#L29
There is no flag or option with this name:
8.18 (fiat-core parsers parsers-examples coq-ci): 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 parsers-examples coq-ci): src/Common/Tactics/IsClosed.v#L1
Trying to mask the absolute name "Coq.Lists.ListSet"!
8.18 (fiat-core parsers parsers-examples coq-ci): src/Common/Tactics/IsClosed.v#L1
Trying to mask the absolute name "Coq.Lists.ListSet"!
8.18 (fiat-core parsers parsers-examples coq-ci): src/Common/Tactics/IsClosed.v#L1
Trying to mask the absolute name "Coq.Lists.ListSet.set_diff_nodup"!
8.18 (fiat-core parsers parsers-examples coq-ci): src/Common/Tactics/PrintContext.v#L1
Trying to mask the absolute name "Coq.Lists.ListSet"!
8.18 (fiat-core parsers parsers-examples coq-ci): src/Common/Tactics/PrintContext.v#L1
Trying to mask the absolute name "Coq.Lists.ListSet"!
8.18 (fiat-core parsers parsers-examples coq-ci): src/Common/Tactics/PrintContext.v#L1
Trying to mask the absolute name "Coq.Lists.ListSet.set_diff_nodup"!
8.18 (fiat-core parsers parsers-examples coq-ci): src/Parsers/StringLike/Core.v#L5
Trying to mask the absolute name "Coq.Lists.ListSet"!
8.17 (fiat-core parsers parsers-examples coq-ci): 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 parsers-examples coq-ci): src/Common/Coq__8_4__8_5__Compat.v#L29
There is no flag or option with this name:
8.17 (fiat-core parsers parsers-examples coq-ci): src/Parsers/StringLike/Core.v#L47
Declaring a scope implicitly is deprecated; use in advance an
8.17 (fiat-core parsers parsers-examples coq-ci): src/Parsers/ExtrOcamlPrimitives.v#L17
Declaring a scope implicitly is deprecated; use in advance an
8.17 (fiat-core parsers parsers-examples coq-ci): src/Computation/Notations.v#L20
Declaring a scope implicitly is deprecated; use in advance an
8.17 (fiat-core parsers parsers-examples coq-ci): src/Common/BoolFacts.v#L11
Declaring a scope implicitly is deprecated; use in advance an
8.17 (fiat-core parsers parsers-examples coq-ci): src/Common/Le.v#L91
Tactic omega is deprecated since 8.12.
8.17 (fiat-core parsers parsers-examples coq-ci): src/Common/Le.v#L94
Tactic omega is deprecated since 8.12.
8.17 (fiat-core parsers parsers-examples coq-ci): src/Common/Le.v#L97
Tactic omega is deprecated since 8.12.
8.17 (fiat-core parsers parsers-examples coq-ci): src/Common/Le.v#L100
Tactic omega is deprecated since 8.12.
8.19 (fiat-core parsers parsers-examples coq-ci): src/Common/Coq__8_4__8_5__Compat.v#L12
There is no flag or option with this name: "Template Check".
8.19 (fiat-core parsers parsers-examples coq-ci): src/Common/Coq__8_4__8_5__Compat.v#L28
There is no flag or option with this name:
8.19 (fiat-core parsers parsers-examples coq-ci): src/Common/Coq__8_4__8_5__Compat.v#L29
There is no flag or option with this name: "Apply With Renaming".
8.19 (fiat-core parsers parsers-examples coq-ci): src/Common/Coq__8_4__8_5__Compat.v#L57
Use of “Require” inside a module is fragile. It is not recommended
8.19 (fiat-core parsers parsers-examples coq-ci): src/Common/Coq__8_4__8_5__Compat.v#L58
Use of “Require” inside a module is fragile. It is not recommended
8.19 (fiat-core parsers parsers-examples coq-ci): src/Common/Coq__8_4__8_5__Compat.v#L59
Use of “Require” inside a module is fragile. It is not recommended
8.19 (fiat-core parsers parsers-examples coq-ci): src/Common/Coq__8_4__8_5__Compat.v#L60
Use of “Require” inside a module is fragile. It is not recommended
8.19 (fiat-core parsers parsers-examples coq-ci): src/Parsers/StringLike/Core.v#L47
Declaring a scope implicitly is deprecated; use in advance an
8.19 (fiat-core parsers parsers-examples coq-ci): src/Parsers/ExtrOcamlPrimitives.v#L17
Declaring a scope implicitly is deprecated; use in advance an
8.19 (fiat-core parsers parsers-examples coq-ci): src/Computation/Notations.v#L20
Declaring a scope implicitly is deprecated; use in advance an
8.16 (fiat-core parsers parsers-examples coq-ci): 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 parsers-examples coq-ci): src/Common/Coq__8_4__8_5__Compat.v#L29
There is no flag or option with this name:
8.16 (fiat-core parsers parsers-examples coq-ci): src/Parsers/StringLike/Core.v#L47
Declaring a scope implicitly is deprecated; use in advance an
8.16 (fiat-core parsers parsers-examples coq-ci): src/Parsers/ExtrOcamlPrimitives.v#L17
Declaring a scope implicitly is deprecated; use in advance an
8.16 (fiat-core parsers parsers-examples coq-ci): src/Computation/Notations.v#L20
Declaring a scope implicitly is deprecated; use in advance an
8.16 (fiat-core parsers parsers-examples coq-ci): src/Common/BoolFacts.v#L11
Declaring a scope implicitly is deprecated; use in advance an
8.16 (fiat-core parsers parsers-examples coq-ci): src/Common/Le.v#L91
Tactic omega is deprecated since 8.12.
8.16 (fiat-core parsers parsers-examples coq-ci): src/Common/Le.v#L94
Tactic omega is deprecated since 8.12.
8.16 (fiat-core parsers parsers-examples coq-ci): src/Common/Le.v#L97
Tactic omega is deprecated since 8.12.
8.16 (fiat-core parsers parsers-examples coq-ci): src/Common/Le.v#L100
Tactic omega is deprecated since 8.12.