set_solver does not unfold is_Some
Example foo : is_Some (({[ 10 := 55 ]} : gmap nat nat) !! 10).
Proof.
Fail set_solver. (* No matching clauses for match. *)
unfold is_Some. set_solver. (* Works. *)
Qed.
Example foo : is_Some (({[ 10 := 55 ]} : gmap nat nat) !! 10).
Proof.
Fail set_solver. (* No matching clauses for match. *)
unfold is_Some. set_solver. (* Works. *)
Qed.