Stream: Coq users

Topic: import categories


view this post on Zulip 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)

view this post on Zulip 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.

view this post on Zulip 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: Feb 08 2023 at 23:03 UTC