Commit 5380a1d7 authored by Ralf Jung's avatar Ralf Jung
Browse files

fix build on Coq 8.11

parent 79074660
......@@ -291,8 +291,8 @@ Lemma gen_heap_init_names `{Countable L, !gen_heapPreG L V Σ} σ :
let hG := GenHeapG L V Σ γh γm in
gen_heap_interp σ ([ map] l v σ, l v) ([ map] l _ σ, meta_token l ).
iMod (ghost_map_alloc_empty (V:=V)) as (γh) "Hh".
iMod (ghost_map_alloc_empty (V:=gname)) as (γm) "Hm".
iMod (ghost_map_alloc_empty (K:=L) (V:=V)) as (γh) "Hh".
iMod (ghost_map_alloc_empty (K:=L) (V:=gname)) as (γm) "Hm".
iExists γh, γm.
iAssert (gen_heap_interp (hG:=GenHeapG _ _ _ γh γm) ) with "[Hh Hm]" as "Hinterp".
{ iExists ; simpl. iFrame "Hh Hm". by rewrite dom_empty_L. }
Supports Markdown
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