Adapt to rocq-prover/rocq#21129.#140
Merged
ppedrot merged 1 commit intoSep 28, 2025
Merged
Annotations
10 warnings
|
implementations/ne_list.v#L8
"Proof term." is deprecated. Use "Proof. exact term. Qed." instead.
|
|
misc/JMrelation.v#L17
"From Coq" has been replaced by "From Stdlib".
|
|
misc/JMrelation.v#L3
Loading Stdlib without prefix is deprecated.
|
|
misc/JMrelation.v#L3
Loading Stdlib without prefix is deprecated.
|
|
implementations/ne_list.v#L3
"From Coq" has been replaced by "From Stdlib".
|
|
misc/stdlib_hints.v#L9
Adding and removing hints in the core database implicitly is
|
|
misc/stdlib_hints.v#L7
Adding and removing hints in the core database implicitly is
|
|
misc/stdlib_hints.v#L4
Adding and removing hints in the core database implicitly is
|
|
misc/stdlib_hints.v#L2
"From Coq" has been replaced by "From Stdlib".
|
|
misc/stdlib_hints.v#L1
"From Coq" has been replaced by "From Stdlib".
|
The logs for this run have expired and are no longer available.
Loading