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