From 83448f762498197a66c448ed1c678591214c32cc Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sat, 3 Jul 2021 16:37:27 +0200
Subject: [PATCH] Make `done` work on `is_Some`.

---
 theories/option.v | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

diff --git a/theories/option.v b/theories/option.v
index a3513f5c..0fd7dfaa 100644
--- a/theories/option.v
+++ b/theories/option.v
@@ -40,12 +40,14 @@ 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.
+
 Lemma is_Some_alt {A} (mx : option A) :
   is_Some mx ↔ match mx with Some _ => True | None => False end.
 Proof. unfold is_Some. destruct mx; naive_solver. Qed.
 
 Lemma mk_is_Some {A} (mx : option A) x : mx = Some x → is_Some mx.
-Proof. intros; red; subst; eauto. Qed.
+Proof. by intros ->. Qed.
 Global Hint Resolve mk_is_Some : core.
 Lemma is_Some_None {A} : ¬is_Some (@None A).
 Proof. by destruct 1. Qed.
@@ -135,7 +137,7 @@ Section setoids.
   Proof. split; [inversion 1; naive_solver|naive_solver (by constructor)]. Qed.
 
   Global Instance is_Some_proper : Proper ((≡@{option A}) ==> iff) is_Some.
-  Proof. inversion_clear 1; split; eauto. Qed.
+  Proof. by inversion_clear 1. Qed.
   Global Instance from_option_proper {B} (R : relation B) :
     Proper (((≡@{A}) ==> R) ==> R ==> (≡) ==> R) from_option.
   Proof. destruct 3; simpl; auto. Qed.
-- 
GitLab