diff --git a/theories/option.v b/theories/option.v
index 0ebd0bf58d0530ba3b27dd09a4b60056637efb2f..37b52505d8ee7b41483350db08d6304964025a34 100644
--- a/theories/option.v
+++ b/theories/option.v
@@ -40,6 +40,7 @@ Proof. congruence. Qed.
 Definition is_Some {A} (mx : option A) := ∃ x, mx = Some x.
 Global Instance: Params (@is_Some) 1 := {}.
 
+(** We avoid calling [done] recursively as that can lead to an unresolved evar. *)
 Global Hint Extern 0 (is_Some _) => eexists; fast_done : core.
 
 Lemma is_Some_alt {A} (mx : option A) :