From fe9fe32a5305d5e002706afacbdf088d89c64dd8 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 15 Jul 2021 14:20:24 +0200
Subject: [PATCH] Test.

---
 tests/tactics.v | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

diff --git a/tests/tactics.v b/tests/tactics.v
index 11d0a3c5..e5eef515 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,8 @@ 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.
-- 
GitLab