From 61840d318d6e147f3d8b8bb635b7235ee6d9c501 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 22 Dec 2016 10:26:21 +0100
Subject: [PATCH] move gen_heap to base_logic. It does not depend on WP or
antyhing language-specific.
---
_CoqProject | 2 +-
theories/{program_logic => base_logic/lib}/gen_heap.v | 0
theories/heap_lang/lifting.v | 3 ++-
3 files changed, 3 insertions(+), 2 deletions(-)
rename theories/{program_logic => base_logic/lib}/gen_heap.v (100%)
diff --git a/_CoqProject b/_CoqProject
index b4ace7a28..e7841b5a0 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -83,6 +83,7 @@ theories/base_logic/lib/na_invariants.v
theories/base_logic/lib/cancelable_invariants.v
theories/base_logic/lib/counter_examples.v
theories/base_logic/lib/fractional.v
+theories/base_logic/lib/gen_heap.v
theories/program_logic/adequacy.v
theories/program_logic/lifting.v
theories/program_logic/weakestpre.v
@@ -91,7 +92,6 @@ theories/program_logic/language.v
theories/program_logic/ectx_language.v
theories/program_logic/ectxi_language.v
theories/program_logic/ectx_lifting.v
-theories/program_logic/gen_heap.v
theories/program_logic/ownp.v
theories/heap_lang/lang.v
theories/heap_lang/tactics.v
diff --git a/theories/program_logic/gen_heap.v b/theories/base_logic/lib/gen_heap.v
similarity index 100%
rename from theories/program_logic/gen_heap.v
rename to theories/base_logic/lib/gen_heap.v
diff --git a/theories/heap_lang/lifting.v b/theories/heap_lang/lifting.v
index 861e50cef..9d3dfeb8f 100644
--- a/theories/heap_lang/lifting.v
+++ b/theories/heap_lang/lifting.v
@@ -1,4 +1,5 @@
-From iris.program_logic Require Export weakestpre gen_heap.
+From iris.base_logic Require Export gen_heap.
+From iris.program_logic Require Export weakestpre.
From iris.program_logic Require Import ectx_lifting.
From iris.heap_lang Require Export lang.
From iris.heap_lang Require Import tactics.
--
GitLab