From 1b5e1bc617a0baa34e5343128134de9b627da80e Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Mon, 16 May 2022 20:18:41 +0200
Subject: [PATCH] use tc_opaque for a complicated definition

---
 iris/base_logic/lib/boxes.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/iris/base_logic/lib/boxes.v b/iris/base_logic/lib/boxes.v
index baf6635d5..1e9283268 100644
--- a/iris/base_logic/lib/boxes.v
+++ b/iris/base_logic/lib/boxes.v
@@ -35,10 +35,10 @@ Section box_defs.
     box_own_prop γ P ∗ inv N (slice_inv γ P).
 
   Definition box (f : gmap slice_name bool) (P : iProp Σ) : iProp Σ :=
-    ∃ Φ : slice_name → iProp Σ,
+    tc_opaque (∃ Φ : slice_name → iProp Σ,
       ▷ (P ≡ [∗ map] γ ↦ _ ∈ f, Φ γ) ∗
       [∗ map] γ ↦ b ∈ f, box_own_auth γ (◯E b) ∗ box_own_prop γ (Φ γ) ∗
-                         inv N (slice_inv γ (Φ γ)).
+                         inv N (slice_inv γ (Φ γ)))%I.
 End box_defs.
 
 Global Instance: Params (@box_own_prop) 3 := {}.
-- 
GitLab