diff --git a/theories/option.v b/theories/option.v
index abdbf6f9f3b6e9847ca256fd2b38b785b9d6b237..f27b31ab34f50f5f5f65c59d91169e10ad59cd86 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 _) => by eexists : core.
+Global Hint Extern 0 (is_Some _) => eexists; reflexivity : core.
 
 Lemma is_Some_alt {A} (mx : option A) :
   is_Some mx ↔ match mx with Some _ => True | None => False end.