Skip to content

do not eta-expand when sealing

Ralf Jung requested to merge ralf/no-eta into master

This changes our uses of sealing to consistently avoid eta-expansion -- except in the proofmode, where I could not figure out what is going on. When I made that sealing conform with our usual patterns, I got conversion errors all over the place (from incorrect unchecked conversion).

Fixes #285 (closed).

Merge request reports