diff --git a/_CoqProject b/_CoqProject
index 1757f9d37abf659873e57e41e329f8520bd296e1..c8698f0dbfcc8ff21318e20054b67c558ac6bb92 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 4ca0d01e22cc10f4c7ac51f07d13b924467cfb11..4c1227febe121e114da08e4835b38896b299bc25 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 0be5893119674191213015c60a98f5186879b861..022e7419e5cd1a151dc308a657a9b1c96a86b149 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