This line should probably use `coq.elaborate-ty-skeleton` instead of `coq.typecheck-ty`

[CohenCyril]

So, this line should probably use coq.elaborate-ty-skeleton instead of coq.typecheck-ty, but I'm unsure what would be its consequences:

hierarchy-builder/HB/builders.elpi

Line 107 in ac1869f

std.assert-ok! (coq.typecheck-ty Package _) Msg,

Originally posted by @pi8027 in math-comp/math-comp#1462 (comment)