Open
Description
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
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