From e353fe431351bb1f41bc6a8c813bea980e8d247c Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Tue, 24 Nov 2020 19:08:53 +0100
Subject: Fixes #13456: regression where tactic exists started to check evars
 incrementally.

The regression was due to #12365. We fix it by postponing the evars
check after the calls to the underlying constructor tactic, while
retaining using information from the first instantiations to resolve
the latter instantiations.
---
 test-suite/bugs/closed/bug_13456.v | 5 +++++
 1 file changed, 5 insertions(+)
 create mode 100644 test-suite/bugs/closed/bug_13456.v

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/bug_13456.v b/test-suite/bugs/closed/bug_13456.v
new file mode 100644
index 0000000000..b2e7fa7be5
--- /dev/null
+++ b/test-suite/bugs/closed/bug_13456.v
@@ -0,0 +1,5 @@
+Lemma minbug (n : nat) (P : nat -> Prop) (pn : P n) : exists (m : nat) (p : P m), True.
+Proof.
+  exists _, pn.
+  exact I.
+Qed.
-- 
cgit v1.2.3