From 5e47e4ce4004229f11899e59fe7d67666876e48f Mon Sep 17 00:00:00 2001 From: Ralf Jung <jung@mpi-sws.org> Date: Tue, 10 Nov 2020 14:29:15 +0100 Subject: [PATCH] rename gen_heap_alloc_gen -> gen_heap_alloc_big --- theories/base_logic/lib/gen_heap.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/theories/base_logic/lib/gen_heap.v b/theories/base_logic/lib/gen_heap.v index 523c5c227..660d2c30e 100644 --- a/theories/base_logic/lib/gen_heap.v +++ b/theories/base_logic/lib/gen_heap.v @@ -265,7 +265,7 @@ Section gen_heap. rewrite !dom_insert_L. set_solver. Qed. - Lemma gen_heap_alloc_gen σ σ' : + Lemma gen_heap_alloc_big σ σ' : σ' ##ₘ σ → gen_heap_interp σ ==∗ gen_heap_interp (σ' ∪ σ) ∗ ([∗ map] l ↦ v ∈ σ', l ↦ v) ∗ ([∗ map] l ↦ _ ∈ σ', meta_token l ⊤). -- GitLab