From 967cda053a36398861c7b48e6295ddc76861602e Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 15 Jul 2021 14:30:11 +0200
Subject: [PATCH] Use `fast_done` as suggested by @jung.

---
 tests/tactics.v   | 4 ++++
 theories/option.v | 2 +-
 2 files changed, 5 insertions(+), 1 deletion(-)

diff --git a/tests/tactics.v b/tests/tactics.v
index e5eef515..715e747d 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 f27b31ab..0ebd0bf5 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.
-- 
GitLab