From def85437a5f388b442a6e9af2d7d0e04860f9629 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 21 Feb 2018 22:11:22 +0100
Subject: [PATCH] Add `tc_opaque` instances for invariants.

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

diff --git a/theories/proofmode/classes.v b/theories/proofmode/classes.v
index 0e8eac3ac..8da87af4b 100644
--- a/theories/proofmode/classes.v
+++ b/theories/proofmode/classes.v
@@ -538,3 +538,7 @@ Instance from_modal_tc_opaque {PROP : bi} (P Q : PROP) :
   FromModal P Q → FromModal (tc_opaque P) Q := id.
 Instance elim_modal_tc_opaque {PROP : bi} φ (P P' Q Q' : PROP) :
   ElimModal φ P P' Q Q' → ElimModal φ (tc_opaque P) P' Q Q' := id.
+Instance into_inv_tc_opaque {PROP : bi} (P : PROP) N :
+  IntoInv P N → IntoInv (tc_opaque P) N := id.
+Instance elim_inv_tc_opaque {PROP : bi} φ (Pinv Pin Pout Q Q' : PROP) :
+  ElimInv φ Pinv Pin Pout Q Q' → ElimInv φ (tc_opaque Pinv) Pin Pout Q Q' := id.
-- 
GitLab