From 2c980e72f1f7de5681379cdab458c6efdac60776 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 15 Jan 2020 13:50:27 +0100
Subject: [PATCH] Add test.

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

diff --git a/tests/proofmode.v b/tests/proofmode.v
index 1100315a6..68fdc957f 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -109,6 +109,10 @@ Lemma test_very_fast_iIntros P :
   ∀ x y : nat, (⌜ x = y ⌝ → P -∗ P)%I.
 Proof. by iIntros. Qed.
 
+Definition tc_opaque_test : PROP := tc_opaque (∀ x : nat, ⌜ x = x ⌝)%I.
+Lemma test_iIntros_tc_opaque : tc_opaque_test.
+Proof. by iIntros (x). Qed.
+
 (** Prior to 0b84351c this used to loop, now `iAssumption` instantiates `R` with
 `False` and performs false elimination. *)
 Lemma test_iAssumption_evar_ex_false : ∃ R, R ⊢ ∀ P, P.
-- 
GitLab