Incorrect parsing in HB.structure Definition ...

[MathisBD]

In HB.structure Definition ... one can use the &} syntax to bring in all implicit dependencies of the mixins of the structure. This however results in a parse error when there are at least two factories in the structure.

Here is a minimal example to reproduce this :

From HB Require Export structures.

HB.mixin Record mixin1 T := {}.
HB.structure Definition struct1 := { T of mixin1 T }.

HB.mixin Record mixin2 T of mixin1 T := {}.
HB.structure Definition struct2 := { T of mixin2 T &}.
(* Works as intended, no warning. *)

HB.mixin Record mixin3 T of mixin2 T & mixin1 T := {}.
HB.structure Definition struct3 := { T of mixin3 T & mixin2 T &}.
(* Parse error. *)