Skip to content
GitLab

Fix scopes of bupd and fupd

Merged Paolo G. Giarrusso requested to merge Blaisorblade/iris:bfupd-scopes into master

BTW, this is missing a simpl never, that is used in derived_connectives.v.

The type_scope might be overkill, but it's inferred and it'd be lost.