mathlib

c2580ebc - refactor(tactic/*): mark internal attrs as `parser := failed` (#8635)

refactor(tactic/*): mark internal attrs as `parser := failed` (#8635) I saw this trick in some of the other user attributes, and it seems like a good idea to apply generally. Any attribute that is "internal use only" should have its `parser` field set to `failed`, so that it is impossible for the user to write the attribute. It is still possible for meta code to set the attributes programmatically, which is generally what's happening anyway.