Make `done` work on `is_Some`. (!293) · Merge requests · Iris / stdpp · GitLab

Snippets Groups Projects

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

Approval is optional

Activity

Robbert Krebbers mentioned in merge request !292 (merged) 3 years ago

mentioned in merge request !292 (merged)
Ralf Jung @jung 3 years ago

Owner

Ah well, I guess that also works. :D
Ralf Jung @jung 3 years ago

Owner

Please add a changelog, other than that LGTM.
Robbert Krebbers added 1 commit 3 years ago
added 1 commit

c45911b3 - CHANGELOG.

Compare with previous version
Robbert Krebbers enabled an automatic merge when the pipeline for c45911b3 succeeds 3 years ago

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

merged
Robbert Krebbers mentioned in commit fb2e3c8e 3 years ago

mentioned in commit fb2e3c8e
Ralf Jung @jung 3 years ago

Owner

@iris-users this could break your proofs because done now solves more goals (namely those of the form is_Some _).
Robbert Krebbers mentioned in merge request !296 (merged) 3 years ago

mentioned in merge request !296 (merged)

Please register or sign in to reply