Honor the #[local] attribute for HB.structure

[CohenCyril]

The local attribute for HB.structure should make sure that the names are not exported in the global environement.

Spotted by @ggonthier

[gares]

The operation names?
I think a silly test could clarify and work as a spec.

[CohenCyril]

Module A.
HB.mixin M T := { op : T }.
#[local] HB.structure S := { T of M T }.
End A.
Import A.
Fail Check op. (* intended behaviour *)
Check A.op.

[gares]

Ok, as in Local Definition op := ..., I think we have the API already, @local! => coq.env.add-const ... should do it.