Update docker-action.yml #77
SkySkimmerAnnotations
30 warnings
|
build (dev):
misc/JMrelation.v#L17
"From Coq" has been replaced by "From Stdlib".
|
|
build (dev):
misc/JMrelation.v#L3
Loading Stdlib without prefix is deprecated.
|
|
build (dev):
misc/JMrelation.v#L3
Loading Stdlib without prefix is deprecated.
|
|
build (dev):
quote/classquote.v#L1
"From Coq" has been replaced by "From Stdlib".
|
|
build (dev):
implementations/ne_list.v#L3
"From Coq" has been replaced by "From Stdlib".
|
|
build (dev):
misc/stdlib_hints.v#L9
Adding and removing hints in the core database implicitly is
|
|
build (dev):
misc/stdlib_hints.v#L7
Adding and removing hints in the core database implicitly is
|
|
build (dev):
misc/stdlib_hints.v#L4
Adding and removing hints in the core database implicitly is
|
|
build (dev):
misc/stdlib_hints.v#L2
"From Coq" has been replaced by "From Stdlib".
|
|
build (dev):
misc/stdlib_hints.v#L1
"From Coq" has been replaced by "From Stdlib".
|
|
build (8.19):
interfaces/canonical_names.v#L41
Adding and removing hints in the core database implicitly is
|
|
build (8.19):
interfaces/canonical_names.v#L39
Adding and removing hints in the core database implicitly is
|
|
build (8.19):
interfaces/canonical_names.v#L37
Adding and removing hints in the core database implicitly is
|
|
build (8.19):
interfaces/canonical_names.v#L30
Notation "_ ≠ _" was already used in scope type_scope.
|
|
build (8.19):
interfaces/canonical_names.v#L26
Declaring a scope implicitly is deprecated; use in advance an
|
|
build (8.19):
interfaces/canonical_names.v#L25
Notation "_ = _" was already used in scope type_scope.
|
|
build (8.19):
interfaces/canonical_names.v#L2
There is no flag or option with this name: "Automatic Introduction".
|
|
build (8.19):
misc/stdlib_hints.v#L9
Adding and removing hints in the core database implicitly is
|
|
build (8.19):
misc/stdlib_hints.v#L7
Adding and removing hints in the core database implicitly is
|
|
build (8.19):
misc/stdlib_hints.v#L4
Adding and removing hints in the core database implicitly is
|
|
build (8.18):
interfaces/canonical_names.v#L41
Adding and removing hints in the core database implicitly is
|
|
build (8.18):
interfaces/canonical_names.v#L39
Adding and removing hints in the core database implicitly is
|
|
build (8.18):
interfaces/canonical_names.v#L37
Adding and removing hints in the core database implicitly is
|
|
build (8.18):
interfaces/canonical_names.v#L30
Notation "_ ≠ _" was already used in scope type_scope.
|
|
build (8.18):
interfaces/canonical_names.v#L26
Declaring a scope implicitly is deprecated; use in advance an
|
|
build (8.18):
interfaces/canonical_names.v#L25
Notation "_ = _" was already used in scope type_scope.
|
|
build (8.18):
interfaces/canonical_names.v#L2
There is no flag or option with this name: "Automatic Introduction".
|
|
build (8.18):
misc/stdlib_hints.v#L9
Adding and removing hints in the core database implicitly is
|
|
build (8.18):
misc/stdlib_hints.v#L7
Adding and removing hints in the core database implicitly is
|
|
build (8.18):
misc/stdlib_hints.v#L4
Adding and removing hints in the core database implicitly is
|