Say two plugins have
VERNAC COMMAND EXTEND for the same command name, is there a reliable way to choose one over the other? Maybe loading one first/last?
In particular there's this issue that Equations and QuickChick both define
Derive. I can add a
QCDerive command, but should I also retire the existing
Derive command, or is there a way for users of both packages to keep using Equation's version regardless?
I also asked here: https://coq.zulipchat.com/#narrow/stream/237977-Coq-users/topic/Disambiguating.20between.20vernaculars.20from.20plugins
So if you load Equations last, you get its
Yep indeed. I think it would make sense to leave everything as it is in QC/Equations but just provide an additional unambiguous vernacular as an alias
Hm, is that better or worse than "loading both plugins is forbidden" like for notations
It depends whether you are looking for an excuse to not work.
Last updated: Feb 05 2023 at 22:03 UTC