Do not call `done` recursively when solving `is_Some`. (!296) · Merge requests · Iris / stdpp · GitLab

Snippets Groups Projects

Merged Robbert Krebbers requested to merge robbert/done_is_Some_non_rec into master 3 years ago

All threads resolved!

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

Activity

Ralf Jung @jung started a thread on an old version of the diff 3 years ago

Resolved 3 years ago by Ralf Jung
Last reply by Robbert Krebbers 3 years ago

Robbert Krebbers added 1 commit 3 years ago

added 1 commit

967cda05 - Use `fast_done` as suggested by @jung.

Compare with previous version

Ralf Jung @jung started a thread on the diff 3 years ago

Resolved 3 years ago by Robbert Krebbers

Robbert Krebbers resolved all threads 3 years ago

resolved all threads

Robbert Krebbers added 1 commit 3 years ago

added 1 commit

53a108a6 - Apply 1 suggestion(s) to 1 file(s)

Compare with previous version

Robbert Krebbers resolved all threads 3 years ago

resolved all threads

Robbert Krebbers enabled an automatic merge when the pipeline for succeeds 3 years ago

enabled an automatic merge when the pipeline for 53a108a6 succeeds

Robbert Krebbers @robbertkrebbers · 3 years ago

Author Owner

Merging!

Robbert Krebbers merged 3 years ago

merged

Robbert Krebbers mentioned in commit 3 years ago

mentioned in commit 0a6ff58a

Please register or sign in to reply