Kazuhiko Sakaguchi

> Yes roughly, except the truncation has no reason to be only for non negative numbers, I would prefer the function in the mixin to be more general, knowing that...

`Cnat`, `Cint`, `truncC`, and `floorC` have been renamed to `Num.nat`, `Num.int`, `Num.trunc`, and `floorR` respectively. I guess we have to relocate `ssrint.int` (or make the dependency from `ssrint` to `ssrnum`...

Almost done except that `floorR` is still not a part of the Archimedean mixin and defined in `ssrint`. I'm not sure what to do about this point.

Here is a summary of possible solutions: 1. Keeping the dependency relation of libraries as is, placing `truncR`, `Rnat`, and `Rint` in `ssrnum`, and placing `floorR` in `ssrint` (the current...

@CohenCyril That is what I meant in solution 3 IIUC.

> Indeed. It was not clear to me whether you were suggesting to remove the file ssrint, which is what I suggest here. I did not suggest removing `ssrint.v`. So...

Currently, ssrnum.v defines both numeric and Archimedean structures, but some notations (e.g., archiNumDomainType) are deprecated there and re-exported from archimedean.v without deprecation. I also had to re-export the canonical declarations...

@proux01 That is missing and the `floor` function has to be redefined to prove it. I will do it before the next MathComp call. Thanks!

MathComp Analysis does not compile anymore with this change: ```coq - File "./theories/reals.v", line 486, characters 8-39: - Error: - In environment - R : realType - x : R...

@CohenCyril I think trying to be backward compatible is a bit painful in this case. Anyway, I agree that we should discuss this in a meeting. Meanwhile, I would like...