Merge branch 'robbert/done_is_Some' into 'master'

Make `done` work on `is_Some`.

See merge request !293

CHANGELOG.md

@@ -108,6 +108,7 @@ API-breaking change is listed.
 - Rename `insert_delete` → `insert_delete_insert`; add new `insert_delete` that
   is consistent with `delete_insert`.
 - Fix statement of `sum_inhabited_r`. (by Paolo G. Giarrusso)
+- Make `done` work on goals of the form `is_Some`.
 
 The following `sed` script should perform most of the renaming
 (on macOS, replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`).

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.