Poor error message in case of nonexhaustive list of dependencies

[silene]

From HB Require Import structures.
HB.mixin Record IsAddComoid A := {}.
HB.structure Definition AddComoid := { A of IsAddComoid A }.
HB.mixin Record IsAbelianGrp A of IsAddComoid A := {}.
HB.structure Definition AbelianGrp := { A of IsAbelianGrp A }.
HB.mixin Record IsRing K of IsAbelianGrp K (*& IsAddComoid K*) := {}.
(* The elpi tactic/command HB.mixin failed without giving a specific error message. Please report this inconvenience to the authors of the program. *)

[gares]

While we fix this, I suggest you stick to class names since they are already transitively closed by definition.