Generalized coercions#420

Open

Tragicus wants to merge 2 commits intomath-comp:masterfrom

Tragicus:proto-coercion

Commits on Jun 27, 2024

declared sort and Pack_ as coercions in HB/structures.v
qvermande
committed
declare axioms_ as typeclass and typeclass option for HB.structure

Tragicus
authored and
qvermande
committed