Skip to content

Make `done` work on `is_Some`.

Robbert Krebbers requested to merge robbert/done_is_Some into master

Merge request reports