The tacticDocs linter #
The tacticDocs environment linter checks that all tactics defined in a module come with
a (nonempty) docstring.
tacticDocs linter #The tacticDocs environment linter checks that all tactics defined in a module come with
a (nonempty) docstring.