From 7db707047bd506fe1676c0c00bc23dab2fb5bf26 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Fri, 8 Jul 2022 09:19:14 -0400
Subject: [PATCH] make an internal lemma local

---
 iris/base_logic/lib/fancy_updates.v | 3 ++-
 iris/base_logic/lib/later_credits.v | 2 +-
 2 files changed, 3 insertions(+), 2 deletions(-)

diff --git a/iris/base_logic/lib/fancy_updates.v b/iris/base_logic/lib/fancy_updates.v
index b9ba2d8a4..f836b8aef 100644
--- a/iris/base_logic/lib/fancy_updates.v
+++ b/iris/base_logic/lib/fancy_updates.v
@@ -116,7 +116,8 @@ Lemma fupd_plain_soundness_no_lc `{!invGpreS Σ} E1 E2 (P: iProp Σ) `{!Plain P}
   (∀ `{Hinv: !invGS Σ} `{!HasNoLc Σ}, ⊢ |={E1,E2}=> P) → ⊢ P.
 Proof.
   iIntros (Hfupd). apply later_soundness. iMod wsat_alloc as (Hw) "[Hw HE]".
-  iMod (lc_alloc 0) as (Hc) "[_ _]".
+  (* We don't actually want any credits, but we need the [lcGS]. *)
+  iMod (later_credits.le_upd.lc_alloc 0) as (Hc) "[_ _]".
   set (Hi := InvG _ Hw Hc false).
   iAssert (|={⊤,E2}=> P)%I as "H".
   { iMod (fupd_mask_subseteq E1) as "_"; first done. iApply Hfupd. by constructor. }
diff --git a/iris/base_logic/lib/later_credits.v b/iris/base_logic/lib/later_credits.v
index e587a1448..acd0190cf 100644
--- a/iris/base_logic/lib/later_credits.v
+++ b/iris/base_logic/lib/later_credits.v
@@ -345,7 +345,7 @@ Module le_upd.
 
   (** You probably do NOT want to use this lemma; use [lc_soundness] if you want
   to actually use [le_upd]! *)
-  Lemma lc_alloc `{!lcGpreS Σ} n :
+  Local Lemma lc_alloc `{!lcGpreS Σ} n :
     ⊢ |==> ∃ _ : lcGS Σ, lc_supply n ∗ £ n.
   Proof.
     rewrite lc_unseal /lc_def lc_supply_unseal /lc_supply_def.
-- 
GitLab