diff --git a/restructuring/analysis/facts/priority_inversion_is_bounded.v b/restructuring/analysis/facts/priority_inversion_is_bounded.v
index 771e3324d42240d77517fbcf406f534a0d7ed4c2..d552b4ec31e06a708a4300a604454f8f10367a76 100644
--- a/restructuring/analysis/facts/priority_inversion_is_bounded.v
+++ b/restructuring/analysis/facts/priority_inversion_is_bounded.v
@@ -2,7 +2,7 @@ Require Import rt.util.all.
 Require Export rt.restructuring.behavior.all.
 Require Import rt.restructuring.analysis.basic_facts.all.
 Require Import rt.restructuring.model.preemption.valid_model.
-Require Import rt.restructuring.model.preemption.preemption_time.
+Require Import rt.restructuring.model.schedule.preemption_time.
 Require Import rt.restructuring.model.preemption.job.parameters.
 Require Import rt.restructuring.model.preemption.task.parameters.
 Require Import rt.restructuring.model.schedule.priority_driven.
diff --git a/restructuring/model/preemption/preemption_time.v b/restructuring/model/schedule/preemption_time.v
similarity index 100%
rename from restructuring/model/preemption/preemption_time.v
rename to restructuring/model/schedule/preemption_time.v
diff --git a/restructuring/model/schedule/priority_driven.v b/restructuring/model/schedule/priority_driven.v
index 59e8b33d31a58c0dea726e7762db138d94e38965..bdee41ea1c96491f7bc334ddf290f0fe33776644 100644
--- a/restructuring/model/schedule/priority_driven.v
+++ b/restructuring/model/schedule/priority_driven.v
@@ -1,5 +1,5 @@
 Require Export rt.restructuring.model.priority.classes.
-Require Export rt.restructuring.model.preemption.preemption_time.
+Require Export rt.restructuring.model.schedule.preemption_time.
 
 (** We now define what it means for a schedule to respect a priority
     in the presence of jobs with non-preemptive segments. *)