set_solver regression: `{[0]} ∪ dom (∅ : gmap nat nat) ≠ ∅` introduces a shelved variable
This script used to work:
Goal {[0]} ∪ dom (∅ : gmap nat nat) ≠ ∅.
Proof. set_solver. Qed.
Now it fails saying there are shelved goals.
Edited by Ralf Jung