From 2a4c815d69f2304262ccac985e391da464222a41 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 1 Feb 2023 16:19:11 +0100
Subject: [PATCH] make some more adequacy helper lemmas local

---
 iris/program_logic/adequacy.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/iris/program_logic/adequacy.v b/iris/program_logic/adequacy.v
index 76851c1f4..41172bf19 100644
--- a/iris/program_logic/adequacy.v
+++ b/iris/program_logic/adequacy.v
@@ -17,7 +17,7 @@ Implicit Types Φs : list (val Λ → iProp Σ).
 
 Notation wptp s t Φs := ([∗ list] e;Φ ∈ t;Φs, WP e @ s; ⊤ {{ Φ }})%I.
 
-Lemma wp_step s e1 σ1 ns κ κs e2 σ2 efs nt Φ :
+Local Lemma wp_step s e1 σ1 ns κ κs e2 σ2 efs nt Φ :
   prim_step e1 σ1 κ e2 σ2 efs →
   state_interp σ1 ns (κ ++ κs) nt -∗
   £ (S (num_laters_per_step ns)) -∗
@@ -84,7 +84,7 @@ Proof.
   rewrite -Nat.add_assoc -(assoc_L app) -replicate_add. by eauto with iFrame.
 Qed.
 
-Lemma wp_not_stuck κs nt e σ ns Φ :
+Local Lemma wp_not_stuck κs nt e σ ns Φ :
   state_interp σ ns κs nt -∗ WP e {{ Φ }} ={⊤, ∅}=∗ ⌜not_stuck e σ⌝.
 Proof.
   rewrite wp_unfold /wp_pre /not_stuck. iIntros "Hσ H".
-- 
GitLab