Stream: math-comp devs

Topic: deprecation of `iter_add`

Christian Doczkal (Apr 18 2021 at 18:41):

I just noticed that compiling my development with mathomp.dev yields the following warning:

Warning: - Warning: Notation iter_add is deprecated since mathcomp 1.12.0.

However, compiling with 1.12.0 does not produce a warning. I don't know why, because I don't see the problem with the deprecate notation at this tag:

Notation "@ 'iter_add'" :=
  (deprecate iter_add iterD) (at level 10, only parsing) : fun_scope.
Notation iter_add := (@iterD _) (only parsing).

Kazuhiko Sakaguchi (Apr 19 2021 at 09:33):

The last line should be Notation iter_add := (@iter_add _) (only parsing). instead. The source of this mistake is that #640 actually does not revert #633 :joy: @Cyril Cohen

Christian Doczkal (Apr 19 2021 at 15:44):

I think this, once again, shows that it was good do abandon the deprecate notation in favor of the mechanism from Coq. :grinning:

Cyril Cohen (Apr 19 2021 at 15:50):

In this case, the fix is to remove the notation only from mathcomp 1.14.0 / 2.0.0 ^^'

Christian Doczkal (Apr 19 2021 at 15:54):

Cyril Cohen said:

In this case, the fix is to remove the notation only from mathcomp 1.14.0 / 2.0.0 ^^'

I don't find a clean-up issue for this. ^^

Cyril Cohen (Apr 19 2021 at 15:58):

good! ;)

Cyril Cohen (Apr 19 2021 at 15:58):

we should bump the deprecation version from the code, just in case though

Last updated: Oct 13 2024 at 01:02 UTC