Adapt to rocq-prover/rocq#20809 (use evar created by evar tactic instead of hard-coded name in unfold_post)
#834
Annotations
10 warnings
|
compcert/lib/Coqlib.v#L861
Notation rev_length is deprecated since 8.20.
|
|
compcert/lib/Coqlib.v#L861
Notation rev_length is deprecated since 8.20.
|
|
compcert/lib/Coqlib.v#L861
Notation rev_length is deprecated since 8.20.
|
|
msl/functors.v#L87
Automatically putting functorFacts in Prop even though it was
|
|
msl/functors.v#L66
Automatically putting functorFacts in Prop even though it was
|
|
msl/functors.v#L48
Automatically putting functorFacts in Prop even though it was
|
|
msl/functors.v#L30
Automatically putting functorFacts in Prop even though it was
|
|
msl/functors.v#L12
Automatically putting functorFacts in Prop even though it was
|
|
msl/sepalg_generators.v#L49
Automatically putting Void in Prop even though it was declared with
|
|
msl/sepalg.v#L104
Automatically putting Flat_alg in Prop even though it was declared
|
The logs for this run have expired and are no longer available.
Loading