diff --git a/theories/proofmode/environments.v b/theories/proofmode/environments.v
index 8aff6e52bad42f10c71266ba5c9f79ce52181ade..14189e61c672751d8bb4fa789fc47f75eefcde8f 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)