Using interp_genarg in tactic notations where possible, instead of an ad-hoc
interpreter.
Removing the useless pattern ident genarg.