affeldt-aist

> Therefore, I guess, the solution would be to put `ssrZ` (and, perhaps, `ssrR`) into a separate small self-contained library? In this case, the strategy would be to have a...

> Okay to separate the package into two. But what would you name them? > infotheo-ssrext and infotheo-infotheo? Keep infotheo for the main package and ssrstd for ssrZ+ssrR (because it...

> > Keep infotheo for the main package and ssrstd for ssrZ+ssrR (because it provides ssr-like naming for standard library's datatypes)? > > ssrstd sounds too generic or strong, doesn't...

> Let's do that (math-comp/analysis#405, math-comp/analysis#406). fyi, those two have been merged

> > > Keep infotheo for the main package and ssrstd for ssrZ+ssrR (because it provides ssr-like naming for standard library's datatypes)? > > > > > > ssrstd sounds...

PR #31 has been merged that provides product category, there is maybe some duplicate to remove from this PR after rebase I guess

~discussion to continue along~ see also meta issue #311

The release managers for mathcomp 1.11.0 think that, given the fact that it depends on an unreleased version of dune (as of March 7), this PR could be postponed to...

> @affeldt-aist Has there been any decision on whether 1.12.0 should maintain compatibility with Coq 8.9 or not? Currently, #599 is milestoned for 1.12.0 and will break compatibility with 8.9....

@TDiazT This solution is indeed mentioned in the first post of this issue.