Commit 2021-08-17 18:30 fefdcf52View on Github →
feat(tactic/lint): add universe linter (#8685)
- The linter checks that there are no bad
max u voccurrences in declarations (bad means that neither
voccur by themselves). See documentation for more details.
meta/rb_map(but this doesn't give any new transitive imports, so it barely matters). I also removed a transitive import from