handle more goals in solve_ndisj

We should only land this after the deadline since solving more goals can break things.

mentioned in merge request iris!712 (merged)

I am confused, you write:

Make solve_ndisj able to solve more goals of the form _ ⊆ ⊤ ∖ _.

And the tests concern such goals. However, the code indicates that you added hints for ## with ∖ on the RHS, and with ∅ on either side. How's that related?

added 11 commits

• 68b6fda7...715cb884 - 10 commits from branch master
• 1fed5e85 - handle more goals in solve_ndisj

Compare with previous version

added 1 commit

• b217790f - handle more goals in solve_ndisj

Compare with previous version

added 1 commit

• 778fe88c - more tests (by Robbert)

Compare with previous version

resolved all threads

LGTM.

merged

mentioned in commit 30283fa0

@iris-users this makes solve_ndisj stronger, which could break proofs that solve those goals by hand. The good kind of breakage. :)