Figure out how to support import categories and comments in Require statements

Open JasonGross opened this issue 4 years ago • 1 comments

The code at https://github.com/JasonGross/coq-tools/blob/9b3989871caa1315854a196f195ab2e4ce1a0c48/import_util.py#L220-L235 does not support comments in From ... Require ... statements. The code at https://github.com/JasonGross/coq-tools/blob/9b3989871caa1315854a196f195ab2e4ce1a0c48/find-bug.py#L822-L829 does not support import categories (https://github.com/coq/coq/pull/14892) nor filtered imports. Neither supports attributes on these statements. We should support these. This might be helped by SerAPI integration (#56)?

Nov 03 '21 16:11 JasonGross

#196 will fix the problem in import_util. try_split_imports will still need work.

Mar 06 '24 23:03 JasonGross