Fix Open/Close scope

Use Open/Close Scope without Local (i.e., export the scope opening) only when the scope corresponds to the main purpose of the module.

Did you check if Iris still compiles with this change?

I tried doing something like this myself, but instead of Local I used Section. That was pretty horrible, since I had to move all notations and hints outside of the section.

Although I'm not a favor of this kind of "dynamic" scoping, for the purpose of this file, I think it's less ugly that the alternative that I pursued. So, I'm fine merging this.

added 1 commit

• a64bf2f0 - Fix Open/Close scope

Compare with previous version

I checked this still works with Iris (and fixed the bug). Merging.

mentioned in commit 07d34651

merged