diff --git a/tests/tactics.v b/tests/tactics.v index 11d0a3c581c2d06f6a9225ee94e2bcb8aca6d745..715e747db6d7b30ac1bbe2d91ac8c18709fcd2c7 100644 --- a/tests/tactics.v +++ b/tests/tactics.v @@ -1,4 +1,4 @@ -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. diff --git a/theories/option.v b/theories/option.v index abdbf6f9f3b6e9847ca256fd2b38b785b9d6b237..37b52505d8ee7b41483350db08d6304964025a34 100644 --- a/theories/option.v +++ b/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.