From a42f1b54c6a14c3567a9580be5ddf3e1cec47465 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 15 Jan 2020 13:46:27 +0100
Subject: [PATCH] Missing `tc_opaque` instance for `FromForall`.

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

diff --git a/theories/proofmode/classes.v b/theories/proofmode/classes.v
index a294222f0..a71e35277 100644
--- a/theories/proofmode/classes.v
+++ b/theories/proofmode/classes.v
@@ -619,6 +619,8 @@ Instance from_exist_tc_opaque {PROP : bi} {A} (P : PROP) (Φ : A → PROP) :
   FromExist P Φ → FromExist (tc_opaque P) Φ := id.
 Instance into_exist_tc_opaque {PROP : bi} {A} (P : PROP) (Φ : A → PROP) :
   IntoExist P Φ → IntoExist (tc_opaque P) Φ := id.
+Instance from_forall_tc_opaque {PROP : bi} {A} (P : PROP) (Φ : A → PROP) :
+  FromForall P Φ → FromForall (tc_opaque P) Φ := id.
 Instance into_forall_tc_opaque {PROP : bi} {A} (P : PROP) (Φ : A → PROP) :
   IntoForall P Φ → IntoForall (tc_opaque P) Φ := id.
 Instance from_modal_tc_opaque {PROP1 PROP2 : bi} {A}
-- 
GitLab