naive_solver does not solve trivial inconsistencies involving is_Some

Example ex1 : is_Some (None : option nat) → False.
Proof.
  Fail naive_solver. (* No matching clauses for match. *)
  unfold is_Some. naive_solver. (* No more goals. *)
Qed.

Example ex2 : is_Some (Some 10).
Proof.
  naive_solver. (* No more goals. *)
Qed.