Merged requested to merge robbert/open_scope_Z into master
I think the
Open Scope Z_scope in
heap_lang.lang is a mistake. While
Zs are often useful when working with HeapLang, I don't think HeapLang should enforce that on users. Furthermore, whether one actually gets an opened
Z_scope or not seems to depend on the import order (see this discussion on Mattermost).
In this MR I thus remove
Open Scope Z_scope. According to grep, after this MR, there are no other scopes that are opened globally (apart from
algebra.base which is to patch up ssreflect).
As a consequence of this change, some
%Z had to be inserted, while it also allowed for some
%nats to be removed.