Hi folks,
I'm continuing the discussion on https://coq.zulipchat.com/#narrow/stream/240550-Dune-devs-.26-users/topic/Dune.203.2E8.20theories.20declarations about a request that I think is orthogonal of the original bug here.
@Ali Caglayan mentions the possibility to actually guess automatically what plugins are in use by a theory.
Before Coq 8.16, that was not easy to do, as the Declare ML Module
syntax didn't include a proper name. However, for Coq 8.16, indeed, if a .v file is using the new syntax, indeed Dune could compute the (plugins ...)
fields needed for the plugins automatically.
So maybe we should document the plan as a Dune issue, and implement this eventually.
Last updated: Oct 13 2024 at 01:02 UTC