From d4b5cd5a490c79ea4d86e72849bb00ef4575bfbb Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 12 Sep 2018 17:24:28 +0200
Subject: [PATCH] Fix confusing name of bound variable.

---
 theories/proofmode/environments.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/theories/proofmode/environments.v b/theories/proofmode/environments.v
index 8aff6e52b..14189e61c 100644
--- a/theories/proofmode/environments.v
+++ b/theories/proofmode/environments.v
@@ -277,8 +277,8 @@ Fixpoint envs_lookup_delete_list {PROP} (remove_persistent : bool)
   | [] => Some (true, [], Δ)
   | j :: js =>
      ''(p,P,Δ') ← envs_lookup_delete remove_persistent j Δ;
-     ''(q,Hs,Δ'') ← envs_lookup_delete_list remove_persistent js Δ';
-     Some ((p:bool) && q, P :: Hs, Δ'')
+     ''(q,Ps,Δ'') ← envs_lookup_delete_list remove_persistent js Δ';
+     Some ((p:bool) && q, P :: Ps, Δ'')
   end.
 
 Definition envs_snoc {PROP} (Δ : envs PROP)
-- 
GitLab