Tentative commit for TacAlias (tactic notations) to register their names.
Don't raise an error when printing intro-patterns in [functional induction].