From 0e1825e2ea4cabd182161903cb78b3851bb96ae2 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 13 Feb 2017 20:46:47 +0100
Subject: [PATCH] Add a test for 9ea6fa45.

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

diff --git a/theories/tests/proofmode.v b/theories/tests/proofmode.v
index 63b55ce51..2c2581979 100644
--- a/theories/tests/proofmode.v
+++ b/theories/tests/proofmode.v
@@ -130,3 +130,11 @@ Proof. iIntros. iAssert False%I with ">[-]" as "[]". done. Qed.
 
 Lemma demo_14 (M : ucmraT) (P : uPred M) : False -∗ P.
 Proof. iIntros "H". done. Qed.
+
+(* Check instantiation and dependent types *)
+Lemma demo_15 (M : ucmraT) (P : ∀ n, vec nat n → uPred M) :
+  (∀ n v, P n v) -∗ ∃ n v, P n v.
+Proof.
+  iIntros "H". iExists _, [#10].
+  iSpecialize ("H" $! _ [#10]). done.
+Qed.
-- 
GitLab