[...] It might be worth writing a script (more robust than the sed script) to do this: it should be possible to write a generic qualify-names Coq.Lists.List.map map List.map . (qualify-names fully-qualified-constant search-text replacement-text list-of-files-or-directories) script that parses .glob files to find instances of the search text which refer to the fully qualified constant, and replaces them. (Presumably coq-lsp could do something similar.)
[...] It might be worth writing a script (more robust than the sed script) to do this: it should be possible to write a generic
qualify-names Coq.Lists.List.map map List.map .(qualify-names fully-qualified-constant search-text replacement-text list-of-files-or-directories) script that parses .glob files to find instances of the search text which refer to the fully qualified constant, and replaces them. (Presumably coq-lsp could do something similar.)In fact, https://github.com/JasonGross/coq-tools/blob/master/coq_tools/absolutize_imports.py could do the job with just minor changes, namely the code at https://github.com/JasonGross/coq-tools/blob/b29cc4488f36e420ff892a7db7333d26219d0db9/coq_tools/import_util.py#L509-L546 needs to get extra arguments for "restrict the search text (cur_code) to this set of constants" and "restrict the fully qualified names (rep_orig) to this set of constants", and then https://github.com/JasonGross/coq-tools/blob/b29cc4488f36e420ff892a7db7333d26219d0db9/coq_tools/absolutize_imports.py#L33 / https://github.com/JasonGross/coq-tools/blob/b29cc4488f36e420ff892a7db7333d26219d0db9/coq_tools/absolutize_imports.py#L47-L56 would have to pass these two new arguments as well as passing something like
mod_remap={'Coq.Lists.List':'List'}(to be constructed from command line arguments). (And then we'd need to pass-ato absolutize all constants and not just imports.Originally posted by @JasonGross in https://github.com/coq/coq/issues/19037#issuecomment-2119267962