diff --git a/theories/base_logic/lib/iprop.v b/theories/base_logic/lib/iprop.v
index 85085273d93a85c808781b8de185ac8e327b041d..cb59e866ba938f0cbce3120d0a5df2f7f4e36b5a 100644
--- a/theories/base_logic/lib/iprop.v
+++ b/theories/base_logic/lib/iprop.v
@@ -62,8 +62,8 @@ 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.
+Typeclasses Opaque gFunctors.singleton gFunctors.app.
 
 Coercion gFunctors.singleton : gFunctor >-> gFunctors.
 Notation "#[ ]" := gFunctors.nil (format "#[ ]").