Stream: Coq users

Topic: ✔ Small typo in warning

view this post on Zulip Pierre Rousselin (Oct 08 2022 at 15:35):

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.

view this post on Zulip Li-yao (Oct 08 2022 at 16:21):

Thanks for the report! This is already fixed upstream https://github.com/coq/coq/issues/16463 :)

view this post on Zulip Notification Bot (Oct 08 2022 at 20:41):

Pierre Rousselin has marked this topic as resolved.

Last updated: Apr 19 2024 at 18:01 UTC