Forwarded from oscar-devel as this will affect all Nemo users. There
are very good reasons for doing this:
Dear all,
a few of us sat together earlier this week to discuss type names in
Oscar and related packages. We'd like to unify them, and also rectify
some things which are mostly historical artifacts.
Our plans so far are described in this HackMD:
<
https://hackmd.io/0hrBHIUrRZG23xiZZ0NCEA?both>
Feel free to ask questions, or suggest further changes or alterations!
Of course this will be a breaking change (or rather a sequence of
breaking changes) that will requires updates and releases to a bunch
of packages. It'll take us a bit, and where possible, we'll try to
provide the old names for backwards compatibility, at least for some
time.
Best wishes
Max
_______________________________________________
Oscar-dev mailing list
Osca...@mathematik.uni-kl.de
https://mail.mathematik.uni-kl.de/mailman/listinfo/oscar-dev