From efc8fb86f73c60e0c3508d0e821e47e1243ec8df Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sun, 29 May 2016 13:41:21 +0200
Subject: [PATCH] COFE on gname.

---
 program_logic/global_functor.v | 1 +
 1 file changed, 1 insertion(+)

diff --git a/program_logic/global_functor.v b/program_logic/global_functor.v
index fb4a555d8..6d534c266 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))).
-- 
GitLab