Make `done` work on `is_Some`.

mentioned in merge request !292 (merged)

Ah well, I guess that also works. :D

Please add a changelog, other than that LGTM.

added 1 commit

enabled an automatic merge when the pipeline for c45911b3 succeeds

merged

mentioned in commit fb2e3c8e

@iris-users this could break your proofs because done now solves more goals (namely those of the form is_Some _).

mentioned in merge request !296 (merged)

Merge request reports