Adapt to rocq-prover/rocq#21129. (#140) #87
ppedrotAnnotations
50 warnings
|
build (rocq/rocq-prover:9.0):
quote/classquote.v#L1
"From Coq" has been replaced by "From Stdlib".
|
|
build (rocq/rocq-prover:9.0):
misc/JMrelation.v#L17
"From Coq" has been replaced by "From Stdlib".
|
|
build (rocq/rocq-prover:9.0):
misc/JMrelation.v#L3
Loading Stdlib without prefix is deprecated.
|
|
build (rocq/rocq-prover:9.0):
misc/JMrelation.v#L3
Loading Stdlib without prefix is deprecated.
|
|
build (rocq/rocq-prover:9.0):
implementations/ne_list.v#L3
"From Coq" has been replaced by "From Stdlib".
|
|
build (rocq/rocq-prover:9.0):
misc/stdlib_hints.v#L9
Adding and removing hints in the core database implicitly is
|
|
build (rocq/rocq-prover:9.0):
misc/stdlib_hints.v#L7
Adding and removing hints in the core database implicitly is
|
|
build (rocq/rocq-prover:9.0):
misc/stdlib_hints.v#L4
Adding and removing hints in the core database implicitly is
|
|
build (rocq/rocq-prover:9.0):
misc/stdlib_hints.v#L2
"From Coq" has been replaced by "From Stdlib".
|
|
build (rocq/rocq-prover:9.0):
misc/stdlib_hints.v#L1
"From Coq" has been replaced by "From Stdlib".
|
|
build (coqorg/coq:8.19):
interfaces/canonical_names.v#L41
Adding and removing hints in the core database implicitly is
|
|
build (coqorg/coq:8.19):
interfaces/canonical_names.v#L39
Adding and removing hints in the core database implicitly is
|
|
build (coqorg/coq:8.19):
interfaces/canonical_names.v#L37
Adding and removing hints in the core database implicitly is
|
|
build (coqorg/coq:8.19):
interfaces/canonical_names.v#L30
Notation "_ ≠ _" was already used in scope type_scope.
|
|
build (coqorg/coq:8.19):
interfaces/canonical_names.v#L26
Declaring a scope implicitly is deprecated; use in advance an
|
|
build (coqorg/coq:8.19):
interfaces/canonical_names.v#L25
Notation "_ = _" was already used in scope type_scope.
|
|
build (coqorg/coq:8.19):
interfaces/canonical_names.v#L2
There is no flag or option with this name: "Automatic Introduction".
|
|
build (coqorg/coq:8.19):
misc/stdlib_hints.v#L9
Adding and removing hints in the core database implicitly is
|
|
build (coqorg/coq:8.19):
misc/stdlib_hints.v#L7
Adding and removing hints in the core database implicitly is
|
|
build (coqorg/coq:8.19):
misc/stdlib_hints.v#L4
Adding and removing hints in the core database implicitly is
|
|
build (coqorg/coq:8.18):
interfaces/canonical_names.v#L41
Adding and removing hints in the core database implicitly is
|
|
build (coqorg/coq:8.18):
interfaces/canonical_names.v#L39
Adding and removing hints in the core database implicitly is
|
|
build (coqorg/coq:8.18):
interfaces/canonical_names.v#L37
Adding and removing hints in the core database implicitly is
|
|
build (coqorg/coq:8.18):
interfaces/canonical_names.v#L30
Notation "_ ≠ _" was already used in scope type_scope.
|
|
build (coqorg/coq:8.18):
interfaces/canonical_names.v#L26
Declaring a scope implicitly is deprecated; use in advance an
|
|
build (coqorg/coq:8.18):
interfaces/canonical_names.v#L25
Notation "_ = _" was already used in scope type_scope.
|
|
build (coqorg/coq:8.18):
interfaces/canonical_names.v#L2
There is no flag or option with this name: "Automatic Introduction".
|
|
build (coqorg/coq:8.18):
misc/stdlib_hints.v#L9
Adding and removing hints in the core database implicitly is
|
|
build (coqorg/coq:8.18):
misc/stdlib_hints.v#L7
Adding and removing hints in the core database implicitly is
|
|
build (coqorg/coq:8.18):
misc/stdlib_hints.v#L4
Adding and removing hints in the core database implicitly is
|
|
build (coqorg/coq:8.20):
interfaces/canonical_names.v#L41
Adding and removing hints in the core database implicitly is
|
|
build (coqorg/coq:8.20):
interfaces/canonical_names.v#L39
Adding and removing hints in the core database implicitly is
|
|
build (coqorg/coq:8.20):
interfaces/canonical_names.v#L37
Adding and removing hints in the core database implicitly is
|
|
build (coqorg/coq:8.20):
interfaces/canonical_names.v#L30
Notation "_ ≠ _" was already used in scope type_scope.
|
|
build (coqorg/coq:8.20):
interfaces/canonical_names.v#L26
Declaring a scope implicitly is deprecated; use in advance an
|
|
build (coqorg/coq:8.20):
interfaces/canonical_names.v#L25
Notation "_ = _" was already used in scope type_scope.
|
|
build (coqorg/coq:8.20):
interfaces/canonical_names.v#L2
There is no flag or option with this name: "Automatic Introduction".
|
|
build (coqorg/coq:8.20):
misc/stdlib_hints.v#L9
Adding and removing hints in the core database implicitly is
|
|
build (coqorg/coq:8.20):
misc/stdlib_hints.v#L7
Adding and removing hints in the core database implicitly is
|
|
build (coqorg/coq:8.20):
misc/stdlib_hints.v#L4
Adding and removing hints in the core database implicitly is
|
|
build (rocq/rocq-prover:dev):
implementations/ne_list.v#L8
"Proof term." is deprecated. Use "Proof. exact term. Qed." instead.
|
|
build (rocq/rocq-prover:dev):
misc/JMrelation.v#L17
"From Coq" has been replaced by "From Stdlib".
|
|
build (rocq/rocq-prover:dev):
misc/JMrelation.v#L3
Loading Stdlib without prefix is deprecated.
|
|
build (rocq/rocq-prover:dev):
misc/JMrelation.v#L3
Loading Stdlib without prefix is deprecated.
|
|
build (rocq/rocq-prover:dev):
implementations/ne_list.v#L3
"From Coq" has been replaced by "From Stdlib".
|
|
build (rocq/rocq-prover:dev):
misc/stdlib_hints.v#L9
Adding and removing hints in the core database implicitly is
|
|
build (rocq/rocq-prover:dev):
misc/stdlib_hints.v#L7
Adding and removing hints in the core database implicitly is
|
|
build (rocq/rocq-prover:dev):
misc/stdlib_hints.v#L4
Adding and removing hints in the core database implicitly is
|
|
build (rocq/rocq-prover:dev):
misc/stdlib_hints.v#L2
"From Coq" has been replaced by "From Stdlib".
|
|
build (rocq/rocq-prover:dev):
misc/stdlib_hints.v#L1
"From Coq" has been replaced by "From Stdlib".
|