diff --git a/theories/base_logic/lib/iprop.v b/theories/base_logic/lib/iprop.v
index e4634323cf55f996e133009827b6883305e2c401..42b53f898bb257242879138deb3ccceeaa2cfc50 100644
--- a/theories/base_logic/lib/iprop.v
+++ b/theories/base_logic/lib/iprop.v
@@ -45,6 +45,7 @@ Definition gFunctors_lookup (Σ : gFunctors) : gid Σ → gFunctor := projT2 Σ.
 Coercion gFunctors_lookup : gFunctors >-> Funclass.
 
 Definition gname := positive.
+Canonical Structure gnameC := leibnizC gname.
 
 (** The resources functor [iResF Σ A := ∀ i : gid, gname -fin-> (Σ i) A]. *)
 Definition iResF (Σ : gFunctors) : urFunctor :=