pull: fix pulling with a hidden tip
Previously, we'd use the filtered repository for determining whether
we pulled any changes. This is incorrect, as tip+1
may be a hidden
commit in that case, triggering an exception on pull. Instead, use the
unfiltered repository.