Skip to content

Remove `Open Scope Z_scope` in HeapLang

Robbert Krebbers 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 general_if_scope in 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.

Edited by Robbert Krebbers

Merge request reports