Kazuhiko Sakaguchi
Kazuhiko Sakaguchi
Sorry, I thought that the (semi)ring structures in `ssralg.v` now inherit from the structures in `monoid.v`, which is not the case. But, a part of the documentation about `nmodType` and...
Ok, I see your point that `ssralg.v` keeps the copy of the stuff moved to `comoid.v`. But, `comoid.v` still lacks some documentation, e.g., `sum`, ``e`_i``, `support`, and `addr_closed`.
I have the impression that what this PR does is not very principled and I prefer to discuss it during the MathComp Sharing Day tomorrow.
https://github.com/math-comp/analysis/pull/1244#discussion_r1679062772 > I'd like to also flip equality lemmas such as ceil_ge0 to have the hand-side with the main identifier on the left. I agree, but general versions of these...
@affeldt-aist Shall we merge? Or do you want me to wait?
FYI, I started porting [lemma-overloading](https://github.com/coq-community/lemma-overloading) to recent versions of Coq and MathComp. I think this is a good stress test for this PR. (I don't think I will finish it...
I suggest rebasing, reviewing, and then merging this PR after merging #1398, without waiting for #1395. Perhaps you can discard (most of) the changes in `matrix.v` since the removal is...
@Tragicus The CI stuff is subsumed by #1443. Can you rebase (and perhaps squash) this PR again?
See also: https://github.com/math-comp/math-comp/pull/1085#issuecomment-1776915476
Hi @proux01 @CohenCyril. IIRC, the plan was to fix this properly during Rocq’n’share. I'm not in Paris, but I'm available for video calls.