fix(tactic/lint): _ is not a linter (#8634)
fix(tactic/lint): _ is not a linter (#8634)

The `#lint` parser accepts `ident_`, but as far as I can tell, `_` doesn't mean anything in particular, it just tries and fails to resolve the `linter._` linter. This simplifies the parser to only accept `ident`.



leanprover-community/mathlib,leanprover-community/mathlib