From 2f67cbdc7be98514e9d8ce77d01e80d8c4476454 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 9 Feb 2016 00:43:46 +0100
Subject: [PATCH] Move upred to algebra as it is not tied to the Iris logic.
---
_CoqProject | 2 +-
{program_logic => algebra}/upred.v | 0
heap_lang/tests.v | 2 +-
program_logic/model.v | 2 +-
4 files changed, 3 insertions(+), 3 deletions(-)
rename {program_logic => algebra}/upred.v (100%)
diff --git a/_CoqProject b/_CoqProject
index 1a54a3ca2..0f233d111 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -49,7 +49,7 @@ algebra/agree.v
algebra/excl.v
algebra/iprod.v
algebra/functor.v
-program_logic/upred.v
+algebra/upred.v
program_logic/model.v
program_logic/adequacy.v
program_logic/hoare_lifting.v
diff --git a/program_logic/upred.v b/algebra/upred.v
similarity index 100%
rename from program_logic/upred.v
rename to algebra/upred.v
diff --git a/heap_lang/tests.v b/heap_lang/tests.v
index 775b4c7f9..b6e50c758 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 program_logic.upred program_logic.ownership.
+Require Import program_logic.ownership.
Require Import heap_lang.lifting heap_lang.sugar.
Import heap_lang uPred notations.
diff --git a/program_logic/model.v b/program_logic/model.v
index a64a8c579..ca0bbec0c 100644
--- a/program_logic/model.v
+++ b/program_logic/model.v
@@ -1,4 +1,4 @@
-Require Export program_logic.upred program_logic.resources.
+Require Export algebra.upred program_logic.resources.
Require Import algebra.cofe_solver.
(* The Iris program logic is parametrized by a functor from the category of
--
GitLab