Slightly better printer for native ML tactics, in order to disambiguate
them.