Merge branch 'robbert/done_is_Some_non_rec' into 'master'

Do not call `done` recursively when solving `is_Some`.

See merge request !296

tests/tactics.v

-From stdpp Require Import tactics.
+From stdpp Require Import tactics option.
 
 Goal ∀ P1 P2 P3 P4 (P: Prop),
   P1 ∨ (Is_true (P2 || P3)) ∨ P4 →
@@ -69,3 +69,12 @@ universe, like [Is_true : bool → Prop]. *)
 Goal True.
 let x := mk_evar true in idtac.
 Abort.
+
+(** Make sure that [done] is not called recursively when solving [is_Some],
+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.

theories/option.v

@@ -40,7 +40,8 @@ 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.
+(** 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) :
   is_Some mx ↔ match mx with Some _ => True | None => False end.