Since 8.16, some warnings indicate that some theorems are deprecated. One of these is :
Warning: Notation minus_plus is deprecated since 8.16.
The Arith.Minus file is obsolete. Use Nat.add_sub (together with Nat.add_com) instead.
I think Nat.add_com
should be Nat.add_comm
.
Thanks for the report! This is already fixed upstream https://github.com/coq/coq/issues/16463 :)
Pierre Rousselin has marked this topic as resolved.
Last updated: Oct 03 2023 at 19:01 UTC