From e2407f9fcaefb73e5f316486a796945c193bd079 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Sat, 18 Apr 2020 22:17:25 +0200
Subject: [PATCH] heap_lang lifting: instantiate inv_heapG and inv_heap_inv

---
 tests/heap_lang.v            | 2 +-
 theories/heap_lang/lifting.v | 5 +++--
 2 files changed, 4 insertions(+), 3 deletions(-)

diff --git a/tests/heap_lang.v b/tests/heap_lang.v
index eca53a8ad..913a9d8c0 100644
--- a/tests/heap_lang.v
+++ b/tests/heap_lang.v
@@ -204,7 +204,7 @@ Section tests.
 End tests.
 
 Section notation_tests.
-  Context `{!heapG Σ, inv_heapG loc val Σ}.
+  Context `{!heapG Σ, !inv_heapG Σ}.
 
   (* Make sure these parse and type-check. *)
   Lemma inv_mapsto_own_test (l : loc) : ⊢ l ↦_(λ _, True) #5. Abort.
diff --git a/theories/heap_lang/lifting.v b/theories/heap_lang/lifting.v
index 814e86d99..3bbdc425a 100644
--- a/theories/heap_lang/lifting.v
+++ b/theories/heap_lang/lifting.v
@@ -1,8 +1,7 @@
 From stdpp Require Import fin_maps.
 From iris.proofmode Require Import tactics.
 From iris.algebra Require Import auth gmap.
-From iris.base_logic.lib Require Export gen_heap proph_map.
-From iris.base_logic.lib Require Import gen_inv_heap.
+From iris.base_logic.lib Require Export gen_heap proph_map gen_inv_heap.
 From iris.program_logic Require Export weakestpre total_weakestpre.
 From iris.program_logic Require Import ectx_lifting total_ectx_lifting.
 From iris.heap_lang Require Export lang.
@@ -35,6 +34,8 @@ Notation "l ↦□ I" := (inv_mapsto (L:=loc) (V:=val) l I%stdpp%type)
   (at level 20, format "l  ↦□  I") : bi_scope.
 Notation "l ↦_ I v" := (inv_mapsto_own (L:=loc) (V:=val) l v I%stdpp%type)
   (at level 20, I at level 9, format "l  ↦_ I   v") : bi_scope.
+Notation inv_heapG := (inv_heapG loc val).
+Notation inv_heap_inv := (inv_heap_inv loc val).
 
 (** The tactic [inv_head_step] performs inversion on hypotheses of the shape
 [head_step]. The tactic will discharge head-reductions starting from values, and
-- 
GitLab