From 0edc1504cf9f28f2f55ec47a16464a5aa318bd0b Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 10 Mar 2020 23:28:40 +0100
Subject: [PATCH] Testcase for
https://gitlab.mpi-sws.org/iris/stdpp/merge_requests/123.
---
opam | 2 +-
tests/proofmode.v | 3 +++
2 files changed, 4 insertions(+), 1 deletion(-)
diff --git a/opam b/opam
index a5cc0c9b4..1b8a693e2 100644
--- a/opam
+++ b/opam
@@ -11,7 +11,7 @@ synopsis: "This is the Coq development of the Iris Project"
depends: [
"coq" { (>= "8.9.1" & < "8.12~") | (= "dev") }
- "coq-stdpp" { (= "dev.2020-03-10.1.20ef8941") | (= "dev") }
+ "coq-stdpp" { (= "dev.2020-03-10.2.8db97649") | (= "dev") }
]
build: [make "-j%{jobs}%"]
diff --git a/tests/proofmode.v b/tests/proofmode.v
index 93876587b..eaf0b0b93 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -227,6 +227,9 @@ Proof.
done.
Qed.
+Lemma test_iSpecialize_evar P : (∀ R, R -∗ R) -∗ P -∗ P.
+Proof. iIntros "H HP". iApply ("H" with "[HP]"). done. Qed.
+
Lemma test_iPure_intro_emp R `{!Affine R} :
R -∗ emp.
Proof. iIntros "HR". by iPureIntro. Qed.
--
GitLab