Skip to content

address deprecation warnings (`iota_add` ➔ `iotaD`)

Björn Brandenburg requested to merge wip-deprecation-warning into master

mathcomp has deprecated iota_add in favor of iotaD.

As iotaD wasn't added until mathcomp 1.12, this patch breaks compatibility with earlier versions, which we just did anyway, so now is a good time to finally merge this.

Some cosmetic cleanups while we're touching the lemma, too.

Does not address deprecation warnings in classic Prosa, which is slowly aging away...

Merge request reports