Notation lost on import when using HB.structure

notation.v

Require Import RelationClasses Morphisms Relation_Definitions.
From HB Require Import structures.

Module M1.
HB.mixin Record Setoid_of_Type A := 
  { eqv : relation A; Eqv : Equivalence eqv }.

HB.structure Definition Setoid := { A of Setoid_of_Type A }.

Declare Scope setoid_scope.
Infix "≡" := eqv (at level 79) : setoid_scope.
Open Scope setoid_scope.
Global Existing Instance Eqv.

Goal forall (X : Setoid.type) (x : X), x ≡ x. Abort. (* OK *)

HB.mixin Record ComMonoid_of_Setoid A of Setoid_of_Type A := 
  { cm_id : A; cm_op : A -> A -> A; cm_laws : True }.
HB.structure Definition ComMonoid := { A of ComMonoid_of_Setoid A & }.

Goal forall (X : Setoid.type) (x : X), x ≡ x. Abort. (* OK *)

End M1.

Import M1.

Goal forall (X : Setoid.type) (x : X), x ≡ x.
(*  forall (X : setoid) (x : X), Elabel.eqv x x *)