From 3cb0702dd9f0d3ed993f90a2a972483bc4d22388 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 10 Nov 2020 15:47:01 +0100
Subject: [PATCH] prefer _L
---
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 a02d41a26..843030241 100644
--- a/theories/base_logic/lib/gen_heap.v
+++ b/theories/base_logic/lib/gen_heap.v
@@ -310,5 +310,5 @@ Proof.
iMod (gen_heap_init ∅) as (gen_heap) "Hinterp". iExists gen_heap.
iMod (gen_heap_alloc_big with "Hinterp") as "(Hinterp & $ & $)".
{ apply map_disjoint_empty_r. }
- rewrite right_id. done.
+ rewrite right_id_L. done.
Qed.
--
GitLab