A bug with insertion of coercions

[dmitromikh]

In the definition of mixin like the next one:

HB.mixin Record foo T := {
  bar : T -> true;
}.

there is an error without any meaningful explanation. However, after the insertion of coercion manually, it works fine:

HB.mixin Record foo T := {
  bar : T -> (is_true true);
}.

So, it would be great if the coercion insertion was automatic.

[CohenCyril]

duplicate of #34