Commit 2021-08-17 18:30 fefdcf52

feat(tactic/lint): add universe linter (#8685)

• The linter checks that there are no bad max u v occurrences in declarations (bad means that neither u nor v occur by themselves). See documentation for more details.
• meta/expr now imports meta/rb_map (but this doesn't give any new transitive imports, so it barely matters). I also removed a transitive import from meta/rb_map.