From e4644041ab96b9dca4cc47dec60cd9a3b08bbd55 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 21 May 2019 23:41:16 +0200
Subject: [PATCH] OFE for gname.

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

diff --git a/theories/base_logic/lib/iprop.v b/theories/base_logic/lib/iprop.v
index e4634323c..42b53f898 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 :=
-- 
GitLab