From aa7e908dd97b15a275c3abe4e2440fa7f795f206 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 13 Apr 2016 00:46:32 +0200
Subject: [PATCH] Rename heap_lang/lib/heap.v -> heap_lang/heap.v
It is not a library; it does not contain code, but instead is a core
part of heap_lang.
---
_CoqProject | 2 +-
heap_lang/{lib => }/heap.v | 0
heap_lang/lib/par.v | 2 +-
heap_lang/lib/spawn.v | 1 -
tests/one_shot.v | 2 +-
5 files changed, 3 insertions(+), 4 deletions(-)
rename heap_lang/{lib => }/heap.v (100%)
diff --git a/_CoqProject b/_CoqProject
index 24194d205..6f9545dde 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -87,7 +87,7 @@ heap_lang/lifting.v
heap_lang/derived.v
heap_lang/notation.v
heap_lang/substitution.v
-heap_lang/lib/heap.v
+heap_lang/heap.v
heap_lang/lib/spawn.v
heap_lang/lib/par.v
heap_lang/lib/assert.v
diff --git a/heap_lang/lib/heap.v b/heap_lang/heap.v
similarity index 100%
rename from heap_lang/lib/heap.v
rename to heap_lang/heap.v
diff --git a/heap_lang/lib/par.v b/heap_lang/lib/par.v
index d65343ef0..962e6c1e2 100644
--- a/heap_lang/lib/par.v
+++ b/heap_lang/lib/par.v
@@ -1,4 +1,4 @@
-From iris.heap_lang Require Export heap spawn.
+From iris.heap_lang Require Export spawn.
From iris.heap_lang Require Import proofmode notation.
Import uPred.
diff --git a/heap_lang/lib/spawn.v b/heap_lang/lib/spawn.v
index d597b0f98..52208d3af 100644
--- a/heap_lang/lib/spawn.v
+++ b/heap_lang/lib/spawn.v
@@ -1,5 +1,4 @@
From iris.program_logic Require Export global_functor.
-From iris.heap_lang Require Export heap.
From iris.proofmode Require Import invariants ghost_ownership.
From iris.heap_lang Require Import proofmode notation.
Import uPred.
diff --git a/tests/one_shot.v b/tests/one_shot.v
index 1ac494639..5134a793c 100644
--- a/tests/one_shot.v
+++ b/tests/one_shot.v
@@ -1,6 +1,6 @@
From iris.algebra Require Import one_shot dec_agree.
From iris.program_logic Require Import hoare.
-From iris.heap_lang Require Import heap assert proofmode notation.
+From iris.heap_lang Require Import assert proofmode notation.
From iris.proofmode Require Import invariants ghost_ownership.
Import uPred.
--
GitLab