Forked from
Iris / stdpp
870 commits behind the upstream repository.
-
Jacques-Henri Jourdan authored
Use Open/Close Scope without Local (i.e., export the scope opening) only when the scope corresponds to the main purpose of the module.
Jacques-Henri Jourdan authoredUse Open/Close Scope without Local (i.e., export the scope opening) only when the scope corresponds to the main purpose of the module.
