From 38abc4499c09f23954cc0e0840d1cb51116e8a9b Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 5 Mar 2019 10:22:55 +0100
Subject: [PATCH] turns out this breaks closed proofs with Let

---
 theories/base_logic/lib/iprop.v | 1 -
 1 file changed, 1 deletion(-)

diff --git a/theories/base_logic/lib/iprop.v b/theories/base_logic/lib/iprop.v
index cb59e866b..67424971d 100644
--- a/theories/base_logic/lib/iprop.v
+++ b/theories/base_logic/lib/iprop.v
@@ -63,7 +63,6 @@ Module gFunctors.
   Definition app (Î£1 Î£2 : gFunctors) : gFunctors :=
     existT (projT1 Î£1 + projT1 Î£2) (fin_plus_inv _ (projT2 Î£1) (projT2 Î£2)).
 End gFunctors.
-Typeclasses Opaque gFunctors.singleton gFunctors.app.
 
 Coercion gFunctors.singleton : gFunctor >-> gFunctors.
 Notation "#[ ]" := gFunctors.nil (format "#[ ]").
-- 
GitLab