From b81fb0fcedcb1420aae8377c87a8f23d8eff78a1 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 15 Jul 2021 14:20:13 +0200
Subject: [PATCH] Do not call `done` recursively when solving `is_Some`.

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

diff --git a/theories/option.v b/theories/option.v
index abdbf6f9..f27b31ab 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.
-- 
GitLab