Skip to content

Do not call `done` recursively when solving `is_Some`.

Robbert Krebbers requested to merge robbert/done_is_Some_non_rec into master

!293 (merged) broke Iris, this MR fixes that.

Merge request reports