From 705d580e894d36b8952a587b761e6936424cae1e Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 3 Feb 2016 16:24:07 +0100
Subject: [PATCH] *oops* forgot to fix imports

---
 heap_lang/heap_lang_tactics.v | 2 +-
 heap_lang/lifting.v           | 2 +-
 heap_lang/sugar.v             | 2 +-
 heap_lang/tests.v             | 2 +-
 4 files changed, 4 insertions(+), 4 deletions(-)

diff --git a/heap_lang/heap_lang_tactics.v b/heap_lang/heap_lang_tactics.v
index f0219d72a..b94d96a98 100644
--- a/heap_lang/heap_lang_tactics.v
+++ b/heap_lang/heap_lang_tactics.v
@@ -1,4 +1,4 @@
-Require Export barrier.heap_lang.
+Require Export heap_lang.heap_lang.
 Require Import prelude.fin_maps.
 Import heap_lang.
 
diff --git a/heap_lang/lifting.v b/heap_lang/lifting.v
index a2bd229f7..883d642f6 100644
--- a/heap_lang/lifting.v
+++ b/heap_lang/lifting.v
@@ -1,5 +1,5 @@
 Require Import prelude.gmap iris.lifting.
-Require Export iris.weakestpre barrier.heap_lang_tactics.
+Require Export iris.weakestpre heap_lang.heap_lang_tactics.
 Import uPred.
 Import heap_lang.
 Local Hint Extern 0 (language.reducible _ _) => do_step ltac:(eauto 2).
diff --git a/heap_lang/sugar.v b/heap_lang/sugar.v
index 92869fe69..36b1ab9dd 100644
--- a/heap_lang/sugar.v
+++ b/heap_lang/sugar.v
@@ -1,4 +1,4 @@
-Require Export barrier.heap_lang barrier.lifting.
+Require Export heap_lang.heap_lang heap_lang.lifting.
 Import uPred.
 Import heap_lang.
 
diff --git a/heap_lang/tests.v b/heap_lang/tests.v
index 667e4f538..c79b53174 100644
--- a/heap_lang/tests.v
+++ b/heap_lang/tests.v
@@ -1,6 +1,6 @@
 (** This file is essentially a bunch of testcases. *)
 Require Import modures.logic.
-Require Import barrier.lifting barrier.sugar.
+Require Import heap_lang.lifting heap_lang.sugar.
 Import heap_lang.
 Import uPred.
 
-- 
GitLab