search

math-comp / hierarchy-builder

High level commands to declare a hierarchy based on packed classes
MIT License
95 stars 20 forks source link

Have a dedicated import category for HB #429

Open CohenCyril opened 1 month ago

CohenCyril commented 1 month ago

When importing, we should be able to be selective about what should or should not be imported from a module/file containing HB declarations, honoring the import category directive of Coq.

Spotted by @ggonthier

gares commented 1 month ago

HB declares Coq standard objects, like CS instances, and Elpi objects (cluases).

Do you want a sort of meta-category encompassing all of these, or be able to give a category name to the Elpi objects?

The former needs to change Coq, the latter Elpi.

CohenCyril commented 1 month ago

I think we need both eventually.

CohenCyril commented 1 month ago

But the latter would already be very useful.