From ae1dd4183426b9163f993f70de56727f4efe2f7e Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 12 Jun 2019 18:49:15 +0200
Subject: [PATCH] `IntoSep` instance for `tc_opaque`.

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

diff --git a/theories/proofmode/classes.v b/theories/proofmode/classes.v
index 5b947614b..5362da96c 100644
--- a/theories/proofmode/classes.v
+++ b/theories/proofmode/classes.v
@@ -612,6 +612,8 @@ Instance from_and_tc_opaque {PROP : bi} (P Q1 Q2 : PROP) :
   FromAnd P Q1 Q2 → FromAnd (tc_opaque P) Q1 Q2 | 102 := id.
 Instance into_and_tc_opaque {PROP : bi} p (P Q1 Q2 : PROP) :
   IntoAnd p P Q1 Q2 → IntoAnd p (tc_opaque P) Q1 Q2 := id.
+Instance into_sep_tc_opaque {PROP : bi} (P Q1 Q2 : PROP) :
+  IntoSep P Q1 Q2 → IntoSep (tc_opaque P) Q1 Q2 := id.
 Instance from_or_tc_opaque {PROP : bi} (P Q1 Q2 : PROP) :
   FromOr P Q1 Q2 → FromOr (tc_opaque P) Q1 Q2 := id.
 Instance into_or_tc_opaque {PROP : bi} (P Q1 Q2 : PROP) :
-- 
GitLab