Closed strub closed 1 month ago
The environment module is currently pre-normalizin module aliases in lemmas & operators. This legacy code was a work-around w.r.t. the glob unsoundness.
This behavior is now useless and kills the benefit of module aliases. This commit removes it.
The environment module is currently pre-normalizin module aliases in lemmas & operators. This legacy code was a work-around w.r.t. the glob unsoundness.
This behavior is now useless and kills the benefit of module aliases. This commit removes it.