math-comp
Deprecating structures/mixins/factories
Although HB comes with the idea of preserving backward compatibility (e.g., by turning a mixin into a factory), we sometimes want to rename (or even remove?) existing structures, mixins, and factories.
For example, we recently renamed a factory of complemented lattices in order.v: https://github.com/math-comp/math-comp/blob/6634f9a81d2882d40b87db3ccb99f79cc14c2b5b/mathcomp/ssreflect/order.v#L4953-L4970 and renamed the HB classes of some archimedean structures: https://github.com/math-comp/math-comp/blob/df3d86612e26e595b9b9c16bd561233f2da33e63/mathcomp/algebra/archimedean.v#L742-L775
As you can see, we have to declare several deprecation notations to deprecate a structure because a structure consists of several Coq declarations. It would be convenient if HB had a command that generates deprecation code like these.
IMO, we unlikely want to remove a structure, but we may want to remove a factory in favor of another factory or mixin when we find the former useless.
If Coq had a feature to deprecate a module, we wouldn't need this feature in HB:
#[deprecated(since="mathcomp 2.3.0")]
Module hasRelativeComplement := BDistrLattice_hasSectionalComplement.