From ad9aa6eb73d499a8842ad29adccc2b295d8d79a8 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Fri, 5 Feb 2016 10:41:44 +0100
Subject: [PATCH] move upred.v into the right folder
---
_CoqProject | 2 +-
heap_lang/tests.v | 2 +-
program_logic/model.v | 2 +-
{logic => program_logic}/upred.v | 0
4 files changed, 3 insertions(+), 3 deletions(-)
rename {logic => program_logic}/upred.v (100%)
diff --git a/_CoqProject b/_CoqProject
index 1757f9d37..c8698f0db 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -41,13 +41,13 @@ algebra/cmra_tactics.v
algebra/sts.v
algebra/auth.v
algebra/fin_maps.v
-logic/upred.v
algebra/cofe.v
algebra/base.v
algebra/dra.v
algebra/cofe_solver.v
algebra/agree.v
algebra/excl.v
+program_logic/upred.v
program_logic/model.v
program_logic/adequacy.v
program_logic/hoare_lifting.v
diff --git a/heap_lang/tests.v b/heap_lang/tests.v
index 4ca0d01e2..4c1227feb 100644
--- a/heap_lang/tests.v
+++ b/heap_lang/tests.v
@@ -1,5 +1,5 @@
(** This file is essentially a bunch of testcases. *)
-Require Import logic.upred.
+Require Import program_logic.upred.
Require Import heap_lang.lifting heap_lang.sugar.
Import heap_lang.
Import uPred.
diff --git a/program_logic/model.v b/program_logic/model.v
index 0be589311..022e7419e 100644
--- a/program_logic/model.v
+++ b/program_logic/model.v
@@ -1,4 +1,4 @@
-Require Export logic.upred program_logic.resources.
+Require Export program_logic.upred program_logic.resources.
Require Import algebra.cofe_solver.
Module iProp.
diff --git a/logic/upred.v b/program_logic/upred.v
similarity index 100%
rename from logic/upred.v
rename to program_logic/upred.v
--
GitLab