Skip to content

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