Adapt to coq/coq#18280 (case relevance outside case info) #541
Annotations
10 warnings
|
src/Rewriter/Util/NatUtil.v#L445
Notation le_plus_minus_r is deprecated since 8.16.
The Arith.Minus file is obsolete. Use Nat.sub_add (together with Nat.add_comm) instead.
|
|
src/Rewriter/Util/NatUtil.v#L445
Notation le_plus_minus_r is deprecated since 8.16.
The Arith.Minus file is obsolete. Use Nat.sub_add (together with Nat.add_comm) instead.
|
|
src/Rewriter/Util/NatUtil.v#L445
Notation le_plus_minus_r is deprecated since 8.16.
The Arith.Minus file is obsolete. Use Nat.sub_add (together with Nat.add_comm) instead.
|
|
src/Rewriter/Util/Tactics2/Ltac1.v#L15
Ltac2 definition get_to_constr is deprecated since 8.15.
Use Ltac2 instead.
|
|
src/Rewriter/Rewriter/Examples/PerfTesting/Sample.v#L749
native_compute disabled at configure time; falling back to
vm_compute.
|
|
src/Rewriter/Util/plugins/Ltac2Extra.v#L9
Trying to mask the absolute name "Ltac2.Constr"!
|
|
src/Rewriter/Util/plugins/Ltac2Extra.v#L10
Trying to mask the absolute name "Ltac2.Constr"!
|
|
src/Rewriter/Language/Reify.v#L67
Trying to mask the absolute name "Ltac2.Ident"!
|
|
src/Rewriter/Language/Reify.v#L68
Trying to mask the absolute name "Ltac2.Ident"!
|
|
src/Rewriter/Language/Reify.v#L310
Ltac2 definition Ltac1.get_to_constr is deprecated since 8.15.
Use Ltac2 instead.
|
The logs for this run have expired and are no longer available.
Loading