I have a project that uses both QuickChick and Equations. Both of these projects define the vernacular Derive X for Y.
in plugins. Is there any way to disambiguate which vernacular I am referring to when I am in a file that has both plugins required?
Depending on how those commands are defined, you can try your luck with Imports.
Or redeclaring the ML modules that define them...
Loading the plugins in the opposite order indeed helps, so this helps, thanks!
One thing I noticed is that this has to be done from the beginning, it seems Declare ML Module
is a no-op for plugins that are already loaded and does not "reoverride" the grammar
I guess that means there is no easy way to resolve the situation where you need both vernaculars in the same file, but that's probably acceptable. Maybe Equations and QuickChick should have some aliases prefixed with Equations and QuickChick to resolve this.
Agreed. Maybe it would be worth to open issues in these projects.
Yep, I'll do that.
Last updated: Oct 13 2024 at 01:02 UTC