From 53a108a610389416423b0e7e40763bb1e1c56505 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 15 Jul 2021 17:59:06 +0000
Subject: [PATCH] Apply 1 suggestion(s) to 1 file(s)

---
 theories/option.v | 1 +
 1 file changed, 1 insertion(+)

diff --git a/theories/option.v b/theories/option.v
index 0ebd0bf5..37b52505 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) :
-- 
GitLab