Fixup: appropriate type for intro-patterns in tacexpr + remove debugging information in pptactic.
In accordance with the definition of the internal [change] tactic, [TacChange] now takes a [delayed_open_constr] rather than a [constr] as an argument.
In accordance with its semantics, [TacRewrite] now takes delayed terms as its input.
More tactics record their names.
Fixup: intro-patterns in inversion use ['dconstr].
Inversion prints its name.