fixes #1182 (renaming Measure_isSFinite_subdef)#1193
fixes #1182 (renaming Measure_isSFinite_subdef)#1193proux01 merged 2 commits intomath-comp:masterfrom
Measure_isSFinite_subdef)#1193Conversation
affeldt-aist
force-pushed
the
fixes_1182
branch
from
24792b5 to
895e2e6
Compare
proux01
left a comment
proux01
left a comment
There was a problem hiding this comment.
Just an orthogonal remark.
I guess if CI is happy, it's fine not to provide deprecation aliases?
theories/measure.v
Outdated
| (* isSFinite == mixin for s-finite measures *) | ||
| (* Measure_isSFinite == factory for s-finite measures *) | ||
| (* isSigmaFinite == mixin corresponding to sigma finiteness *) |
There was a problem hiding this comment.
Do we want to document factories? It seems that in mathcomp the choice was to document structures and tell users to use HB.howto, HB.about,...
In any case we shouldn't distinguish mixins and factories in the doc.
There was a problem hiding this comment.
Do we want to document factories?
Not sure. measure.v predates MathComp 2 so surely we did not have the discipline.
Yet, because of a "circularity" in the definition of s-finite measures, measure.v is doing something special
so I would be inclined to keep the potentially redundant information here.
In any case we shouldn't distinguish mixins and factories in the doc.
I addressed this by changing everything to "interface".
In the process, I found an error in the doc and also fixed three inconsistencies in the naming of other interfaces.
I added them, just in case. |
2 participants
Motivation for this change
fixes #1182
what about this renaming @proux01 ?
Checklist
CHANGELOG_UNRELEASED.mdReference: How to document
Reminder to reviewers