Honor the #[local] attribute for HB.structure

math-comp / hierarchy-builder

High level commands to declare a hierarchy based on packed classes

MIT License

97 stars 20 forks source link

Open CohenCyril opened 4 weeks ago

CohenCyril commented 4 weeks ago

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

Spotted by @ggonthier

gares commented 4 weeks ago

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

CohenCyril commented 4 weeks ago

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 commented 4 weeks ago

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