Avoid type-level aliases for overloading of canonical structures
In !187 (comment 36185) @jjourdan expressed his dissatisfaction with the current means of overloading canonical structures:
I have to say that I really don't like the idea of overloading a canonical structure for a type... Why cannot we define
ufrac
as something like:Record ufrac := uf_qp { qp_uf : Qp }.
? Sure, this will require some boilerplate for projecting and boxing fractions, but hoping that such hack will keep a stable behaviors seems rather optimistic!
This applies to ufrac
(introduced in !195 (merged)) and mnat
(introduced a long time ago).