Gaëtan Gilbert (Feb 09 2022 at 12:42): Gaëtan Gilbert (Feb 09 2022 at 12:42):is the bug mentioned in https://github.com/coq/coq/commit/870d81c699b5d15420a03f2006a7938a158c09a8 reopened?
Enrico Tassi (Feb 09 2022 at 13:18):It depends if the load paths are now part of the summary or not (at that time, they were not)
Enrico Tassi (Feb 09 2022 at 13:19):I believe they should, otherwise Undo has no effect on that command
Gaëtan Gilbert (Feb 09 2022 at 13:25):but we link plugins before we unfreeze the normal summaries so how does it matter if the loadpath is in the summary?
Gaëtan Gilbert (Feb 09 2022 at 13:25):https://github.com/coq/coq/blob/68b485ff65da34764016e8e1b2570e9d20f7566c/library/summary.ml#L81-L86
Enrico Tassi (Feb 09 2022 at 13:38):Right, so one more reason to ditch Add LoadPath
Last updated: Oct 13 2024 at 01:02 UTC