Skip to content
Snippets Groups Projects
Commit 3cb0702d authored by Ralf Jung's avatar Ralf Jung
Browse files

prefer _L

parent 8008c189
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
theories/base_logic/lib/gen_heap.v
+ 1
− 1
View file @ 3cb0702d
...@@ -310,5 +310,5 @@ Proof. ...@@ -310,5 +310,5 @@ Proof.
iMod (gen_heap_init ∅) as (gen_heap) "Hinterp". iExists gen_heap. iMod (gen_heap_init ∅) as (gen_heap) "Hinterp". iExists gen_heap.
iMod (gen_heap_alloc_big with "Hinterp") as "(Hinterp & $ & $)". iMod (gen_heap_alloc_big with "Hinterp") as "(Hinterp & $ & $)".
{ apply map_disjoint_empty_r. } { apply map_disjoint_empty_r. }
rewrite right_id. done. rewrite right_id_L. done.
Qed. Qed.
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