From 0e7930c6aa90053f0a78977b8c4134522ecde8ea Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 25 Mar 2021 13:54:32 +0100
Subject: [PATCH] add test for dependent nested exist

---
 tests/proofmode.v | 9 ++++++++-
 1 file changed, 8 insertions(+), 1 deletion(-)

diff --git a/tests/proofmode.v b/tests/proofmode.v
index 97aa9604a..9d5336d56 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -480,11 +480,18 @@ Proof.
 Qed.
 
 (* Ensure that [% %] works as a pattern for an existential with a pure body. *)
-Lemma test_exist_pure_destruct :
+Lemma test_exist_pure_destruct_1 :
   (∃ x, ⌜ x = 0 ⌝) ⊢@{PROP} True.
 Proof.
   iIntros "[% %]". done.
 Qed.
+(* Also test nested existentials where the type of the 2nd depends on the first
+(which could cause trouble if we do things in the wrong order) *)
+Lemma test_exist_pure_destruct_2 :
+  (∃ x (_:x=0), True) ⊢@{PROP} True.
+Proof.
+  iIntros "(% & % & $)".
+Qed.
 
 Lemma test_fresh P Q:
   (P ∗ Q) -∗ (P ∗ Q).
-- 
GitLab