From 6f3b57de7bbeb567732c8aabbf8f8ce1f0f86e2d Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Sun, 3 Mar 2019 16:39:52 +0100
Subject: [PATCH] tweak GFunctor

---
 theories/base_logic/lib/iprop.v | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/theories/base_logic/lib/iprop.v b/theories/base_logic/lib/iprop.v
index 2ca017324..85085273d 100644
--- a/theories/base_logic/lib/iprop.v
+++ b/theories/base_logic/lib/iprop.v
@@ -30,6 +30,7 @@ Structure gFunctor := GFunctor {
 }.
 Arguments GFunctor _ {_}.
 Existing Instance gFunctor_contractive.
+Add Printing Constructor gFunctor.
 
 (** The type [gFunctors] describes the parameters [Σ] of the Iris logic: lists
 of [gFunctor]s.
@@ -61,6 +62,7 @@ Module gFunctors.
 
   Definition app (Σ1 Σ2 : gFunctors) : gFunctors :=
     existT (projT1 Σ1 + projT1 Σ2) (fin_plus_inv _ (projT2 Σ1) (projT2 Σ2)).
+  Global Typeclasses Opaque singleton app.
 End gFunctors.
 
 Coercion gFunctors.singleton : gFunctor >-> gFunctors.
-- 
GitLab