From c44ce4c974f3b1ed63ffb4cbf12a3cc6645ffa6f Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 29 Nov 2022 14:25:21 +0100
Subject: [PATCH] make lc_supply Local

---
 iris/base_logic/lib/later_credits.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/iris/base_logic/lib/later_credits.v b/iris/base_logic/lib/later_credits.v
index 09b55d1c7..318fd089f 100644
--- a/iris/base_logic/lib/later_credits.v
+++ b/iris/base_logic/lib/later_credits.v
@@ -40,7 +40,7 @@ Notation "'£'  n" := (lc n) (at level 1).
   Users should not directly interface with this. *)
 Local Definition lc_supply_def `{!lcGS Σ} (n : nat) : iProp Σ := own lcGS_name (● n).
 Local Definition lc_supply_aux : seal (@lc_supply_def). Proof. by eexists. Qed.
-Definition lc_supply := lc_supply_aux.(unseal).
+Local Definition lc_supply := lc_supply_aux.(unseal).
 Local Definition lc_supply_unseal :
   @lc_supply = @lc_supply_def := lc_supply_aux.(seal_eq).
 Global Arguments lc_supply {Σ _} n.
-- 
GitLab