Pierre-Marie Pédrot

En passant we also use the registering mechanism for the ring/field tactics. Hopefully it will not be too disruptive. Backwards compatible overlays: - https://github.com/coq-community/atbr/pull/45 - https://github.com/damien-pous/relation-algebra/pull/46

We do not provide a compatibility alias because this is a fairly internal module. It is unlikely that somebody uses it outside of the Coq codebase, but the CI will...