From 84444c5127467e7d2ba516c6f434013f838e4b6f Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 3 Dec 2018 19:36:51 +0100
Subject: [PATCH] Remove unused bound variable.

Thanks @jtassaro.
---
 theories/program_logic/adequacy.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/theories/program_logic/adequacy.v b/theories/program_logic/adequacy.v
index b448661ab..fdbb25a23 100644
--- a/theories/program_logic/adequacy.v
+++ b/theories/program_logic/adequacy.v
@@ -158,7 +158,7 @@ Proof.
   - iDestruct "Ht" as "(_ & He2 & _)". by iMod (wp_safe with "Hσ He2").
 Qed.
 
-Lemma wptp_invariance φ s n e1 κs κs' e2 t1 t2 σ1 σ2 Φ :
+Lemma wptp_invariance φ s n e1 κs κs' t1 t2 σ1 σ2 Φ :
   nsteps n (e1 :: t1, σ1) κs (t2, σ2) →
   (state_interp σ2 κs' (pred (length t2)) ={⊤,∅}=∗ ⌜φ⌝) -∗
   state_interp σ1 (κs ++ κs') (length t1) -∗
-- 
GitLab