Commit d4b5cd5a authored by Robbert Krebbers's avatar Robbert Krebbers

Fix confusing name of bound variable.

parent c25f4d65
......@@ -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)
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment