diff --git a/program_logic/global_functor.v b/program_logic/global_functor.v
index fb4a555d87cc409306c4475e98ccf137fcaffde2..6d534c266cdbfe4c294b128aca05a682e9e1db9d 100644
--- a/program_logic/global_functor.v
+++ b/program_logic/global_functor.v
@@ -16,6 +16,7 @@ Definition gid (Σ : gFunctors) := fin (projT1 Σ).
 
 (** Name of one instance of a particular CMRA in the ghost state. *)
 Definition gname := positive.
+Canonical Structure gnameC := leibnizC gname.
 
 Definition globalF (Σ : gFunctors) : iFunctor :=
   IFunctor (iprodURF (λ i, gmapURF gname (projT2 Σ i))).