Li-yao (Nov 24 2020 at 13:56): Li-yao (Nov 24 2020 at 13:56):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?
Jakob Botsch Nielsen (Nov 24 2020 at 13:58):I also asked here: https://coq.zulipchat.com/#narrow/stream/237977-Coq-users/topic/Disambiguating.20between.20vernaculars.20from.20plugins
Li-yao (Nov 24 2020 at 14:04):So if you load Equations last, you get its Derive?
Jakob Botsch Nielsen (Nov 24 2020 at 14:09):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
Paolo Giarrusso (Nov 24 2020 at 16:42):Hm, is that better or worse than "loading both plugins is forbidden" like for notations
Li-yao (Nov 24 2020 at 16:44):It depends whether you are looking for an excuse to not work.
Last updated: Sep 15 2024 at 13:02 UTC