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: Dec 01 2023 at 06:01 UTC