Gaëtan Gilbert (Sep 16 2021 at 11:55): Gaëtan Gilbert (Sep 16 2021 at 11:55):A feature allowing to import subsets of modules by categories is coming soon; eg import only coercions or import everything except notations (where "coercions" and "notations" are categories)
What import-time effects do you want categories for?
(cf https://github.com/coq/coq/pull/14892)
Enrico Tassi (Sep 16 2021 at 12:16):I've one request, but maybe it's too specific to my use case. In Coq-Elpi I do add a few libobjects. It would be nice if I could flag their declaration as ~category:"elpi" and then have this category to be available in the Import vernac.
Gaëtan Gilbert (Sep 16 2021 at 15:40):Enrico Tassi said:
I've one request, but maybe it's too specific to my use case. In Coq-Elpi I do add a few libobjects. It would be nice if I could flag their declaration as
~category:"elpi"and then have this category to be available in the Import vernac.
if it's the object at https://github.com/LPCIC/coq-elpi/blob/8f60397e29c70cd8c8d5550cac9a5a51677651fd/src/coq_elpi_vernacular.ml#L296 it's just a matter of adding let cat = Libobject.create_category "elpi" somewhere and replacing simple_open by simple_open ~cat in the open_function
see also https://github.com/coq/coq/commit/18be4130f56dde13786e14bfd45ee0378c314d62
Last updated: Sep 28 2023 at 10:01 UTC