diff --git a/tests/tactics.v b/tests/tactics.v
index e5eef5152e57a9b006397c9bd4337aa08c60c93f..715e747db6d7b30ac1bbe2d91ac8c18709fcd2c7 100644
--- a/tests/tactics.v
+++ b/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.
diff --git a/theories/option.v b/theories/option.v
index f27b31ab34f50f5f5f65c59d91169e10ad59cd86..0ebd0bf58d0530ba3b27dd09a4b60056637efb2f 100644
--- a/theories/option.v
+++ b/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.