floor and ceil to be subsumed by MathComp

Open affeldt-aist opened this issue 4 years ago • 1 comments

TODO: revise the use of floor and ceil once ~~math-comp/math-comp#682 is merged into MathComp~~ requiring MC >= 2.1.0

Jan 27 '21 03:01 affeldt-aist

From version 1.2.0, we'll support MathComp >= 2.1, so it is about time to make this change. The deprecation warnings have been removed so that now the expressions to be subsumed appear as reals.blah (e.g., reals.floor, reals.ceil, etc. as in https://github.com/math-comp/analysis/blob/master/theories/normedtype.v#L255).

May 20 '24 05:05 affeldt-aist