Add `set_solver` support for `dom`

This MR closes issue #53 (closed).

@Armael can you review/check if this sufficient for what you had in mind?

added 1 commit

• 8e949e3c - CHANGELOG entry.

Compare with previous version

Would it make sense to add some testcases, like at least the example from #53 (closed)?

Sure can do. @Armael if you have some more tests, could you post them here? Otherwise I'll cook up some.

Right now I don't have more test-cases, sorry. The changes do look good to me, in any case. Thanks!

Here's a test (coGset has an opaque dom):

Goal ∀ X, dom (coGset positive) (∅ : gmap positive unit) ## X.
Proof. Fail set_solver.

It looks like set_solver will no longer fail with this goal.

added 1 commit

• 5f26f6cd - Add tests for `set_solver` on `dom`.

Compare with previous version

changed the description

Added the test from #53 (closed) and @swasey's example. Merging.

merged

mentioned in commit 4fc67339