make solve_ndisj work on goals of the form 'X1 ∪ X2 ## Y' (!427) · Merge requests · Iris / stdpp · GitLab

Snippets Groups Projects

Merged Ralf Jung requested to merge ralf/solve_ndisj into master 2 years ago

All threads resolved!

Activity

Ralf Jung added 14 commits 2 years ago
added 14 commits

8998acb4...d4458085 - 12 commits from branch master

81766ef4 - make solve_ndisj work on goals of the form 'X1 ∪ X2 ## Y'

da9205f9 - add another testcase from iris.program_logic.atomic

Compare with previous version
Ralf Jung @jung started a thread on the diff 2 years ago

Resolved 2 years ago by Ralf Jung
Last reply by Ralf Jung 2 years ago

Robbert Krebbers @robbertkrebbers started a thread on an old version of the diff 2 years ago

Resolved 2 years ago by Ralf Jung

Robbert Krebbers @robbertkrebbers started a thread on an old version of the diff 2 years ago

Resolved 2 years ago by Ralf Jung

Robbert Krebbers @robbertkrebbers · 2 years ago

Owner

LGTM.

Ralf Jung added 1 commit 2 years ago

added 1 commit

807bed4b - linebreaks

Compare with previous version

Ralf Jung resolved all threads 2 years ago

resolved all threads

Ralf Jung merged 2 years ago

merged

Ralf Jung mentioned in commit 2 years ago

mentioned in commit 4763d18a

Please register or sign in to reply