Tactics defined through TACTIC EXTEND that are only defined as a string do
not create grammar and printing rules anymore, they define Ltac entries
in the module that declares them instead.