Use `fast_done` as suggested by @jung.

tests/tactics.v

@@ -74,3 +74,7 @@ Abort.
 which might leave an unresolved evar before performing ex falso. *)
 Goal False → is_Some (@None nat).
 Proof. done. Qed.
+Goal ∀ mx, mx = Some 10 → is_Some mx.
+Proof. done. Qed.
+Goal ∀ mx, Some 10 = mx → is_Some mx.
+Proof. done. Qed.

theories/option.v

@@ -40,7 +40,7 @@ Proof. congruence. Qed.
 Definition is_Some {A} (mx : option A) := ∃ x, mx = Some x.
 Global Instance: Params (@is_Some) 1 := {}.
 
-Global Hint Extern 0 (is_Some _) => eexists; reflexivity : core.
+Global Hint Extern 0 (is_Some _) => eexists; fast_done : core.
 
 Lemma is_Some_alt {A} (mx : option A) :
   is_Some mx ↔ match mx with Some _ => True | None => False end.