I wrote a [**(how-to)**](https://github.com/math-comp/math-comp/wiki/How-to-declare-MathComp-instances) guide on connecting user-developed theories with MathComp ones, using the Hierarchy Builder.
July 24, 2024
You can find it on MathComp’s wiki, here is a link to the guide.