diff --git a/restructuring/analysis/abstract/core/abstract_rta.v b/restructuring/analysis/abstract/core/abstract_rta.v
index fe5bd0e9e516c0db70d07768abb63a2cb5341245..68a2ebaa5b091484f730cb372e412ddcf8a5a241 100644
--- a/restructuring/analysis/abstract/core/abstract_rta.v
+++ b/restructuring/analysis/abstract/core/abstract_rta.v
@@ -4,7 +4,7 @@ Require Import rt.restructuring.analysis.definitions.job_properties.
 Require Import rt.restructuring.model.task.concept.
 Require Import rt.restructuring.model.preemption.valid_model.
 Require Import rt.restructuring.model.preemption.job.parameters.
-Require Import rt.restructuring.model.preemption.task.parameters.
+Require Import rt.restructuring.model.task.preemption.parameters.
 Require Import rt.restructuring.model.preemption.rtc_threshold.valid_rtct.
 Require Import rt.restructuring.analysis.basic_facts.preemption.rtc_threshold.job_preemptable.
 Require Import rt.restructuring.analysis.schedulability.
diff --git a/restructuring/analysis/abstract/core/abstract_seq_rta.v b/restructuring/analysis/abstract/core/abstract_seq_rta.v
index b28114eb035613c3a00eb7529d876d9807612d49..425abc47431dd84f169e0b567bae96c3feb1ebd3 100644
--- a/restructuring/analysis/abstract/core/abstract_seq_rta.v
+++ b/restructuring/analysis/abstract/core/abstract_seq_rta.v
@@ -5,7 +5,7 @@ Require Import rt.restructuring.model.task.concept.
 Require Import rt.restructuring.model.preemption.rtc_threshold.valid_rtct.
 Require Import rt.restructuring.model.preemption.valid_model.
 Require Import rt.restructuring.model.preemption.job.parameters.
-Require Import rt.restructuring.model.preemption.task.parameters.
+Require Import rt.restructuring.model.task.preemption.parameters.
 Require Import rt.restructuring.analysis.basic_facts.preemption.rtc_threshold.job_preemptable.
 Require Import rt.restructuring.model.arrival.arrival_curves.
 
diff --git a/restructuring/analysis/basic_facts/preemption/job/limited.v b/restructuring/analysis/basic_facts/preemption/job/limited.v
index c10c941336bca54c93b2410cf7c57d37d0e9e28f..41f1276cfa62e8bc18bc7d957241c2129a399007 100644
--- a/restructuring/analysis/basic_facts/preemption/job/limited.v
+++ b/restructuring/analysis/basic_facts/preemption/job/limited.v
@@ -6,7 +6,7 @@ Require Import rt.restructuring.model.task.concept.
 Require Import rt.restructuring.model.preemption.valid_model.
 Require Import rt.restructuring.model.preemption.valid_schedule.
 Require Import rt.restructuring.model.preemption.job.parameters.
-Require Import rt.restructuring.model.preemption.task.parameters.
+Require Import rt.restructuring.model.task.preemption.parameters.
 Require Import rt.restructuring.model.preemption.rtc_threshold.valid_rtct.
 Require Import rt.restructuring.model.preemption.job.instance.limited.
 
diff --git a/restructuring/analysis/basic_facts/preemption/job/preemptive.v b/restructuring/analysis/basic_facts/preemption/job/preemptive.v
index 912879604f9433ea709e9f700571af0074009b62..1392a0cfb06a5865c168e9a37a0e30e3c655853f 100644
--- a/restructuring/analysis/basic_facts/preemption/job/preemptive.v
+++ b/restructuring/analysis/basic_facts/preemption/job/preemptive.v
@@ -2,7 +2,7 @@ Require Import rt.util.all.
 Require Import rt.restructuring.behavior.all.
 Require Import rt.restructuring.model.preemption.valid_model.
 Require Import rt.restructuring.model.preemption.job.parameters.
-Require Import rt.restructuring.model.preemption.task.parameters.
+Require Import rt.restructuring.model.task.preemption.parameters.
 Require Import rt.restructuring.model.preemption.job.instance.preemptive.
 
 (** * Preemptions in Fully Premptive Model *)
diff --git a/restructuring/analysis/basic_facts/preemption/rtc_threshold/floating.v b/restructuring/analysis/basic_facts/preemption/rtc_threshold/floating.v
index 31d9f79259778e27c22e14071a02f9d43adebcc2..d7c2bcfd5fc085d16df5bceaefd2c127a58ecd00 100644
--- a/restructuring/analysis/basic_facts/preemption/rtc_threshold/floating.v
+++ b/restructuring/analysis/basic_facts/preemption/rtc_threshold/floating.v
@@ -3,7 +3,7 @@ Require Import rt.restructuring.behavior.all.
 Require Import rt.restructuring.analysis.definitions.job_properties.
 Require Import rt.restructuring.model.task.concept.
 Require Import rt.restructuring.model.preemption.job.parameters.
-Require Import rt.restructuring.model.preemption.task.parameters.
+Require Import rt.restructuring.model.task.preemption.parameters.
 Require Import rt.restructuring.model.preemption.rtc_threshold.valid_rtct.
 Require Import rt.restructuring.model.preemption.job.instance.limited.
 Require Import rt.restructuring.model.preemption.task.instance.floating.
diff --git a/restructuring/analysis/basic_facts/preemption/rtc_threshold/job_preemptable.v b/restructuring/analysis/basic_facts/preemption/rtc_threshold/job_preemptable.v
index 63689bce16f21afae33708aff2cc2b63872a95f8..f446e860d78ca896bb7e2ce37ec956b3ed49cf1b 100644
--- a/restructuring/analysis/basic_facts/preemption/rtc_threshold/job_preemptable.v
+++ b/restructuring/analysis/basic_facts/preemption/rtc_threshold/job_preemptable.v
@@ -4,7 +4,7 @@ Require Import rt.restructuring.model.task.concept.
 Require Import rt.restructuring.analysis.basic_facts.all.
 Require Import rt.restructuring.model.preemption.valid_model.
 Require Import rt.restructuring.model.preemption.job.parameters.
-Require Import rt.restructuring.model.preemption.task.parameters.
+Require Import rt.restructuring.model.task.preemption.parameters.
 
 (** * Run-to-Completion Threshold *) 
 (** In this section, we provide a few basic properties 
diff --git a/restructuring/analysis/basic_facts/preemption/rtc_threshold/limited.v b/restructuring/analysis/basic_facts/preemption/rtc_threshold/limited.v
index f71f40c61aafb19b1b6a2f520762373e04f006fd..c314938786fbe9741d5e2786aca774d292c23fea 100644
--- a/restructuring/analysis/basic_facts/preemption/rtc_threshold/limited.v
+++ b/restructuring/analysis/basic_facts/preemption/rtc_threshold/limited.v
@@ -6,7 +6,7 @@ Require Import rt.restructuring.model.task.concept.
 Require Import rt.restructuring.model.preemption.rtc_threshold.valid_rtct.
 Require Import rt.restructuring.model.preemption.valid_schedule.
 Require Import rt.restructuring.model.preemption.job.parameters.
-Require Import rt.restructuring.model.preemption.task.parameters.
+Require Import rt.restructuring.model.task.preemption.parameters.
 Require Import rt.restructuring.model.preemption.job.instance.limited.
 Require Import rt.restructuring.model.preemption.task.instance.limited.
 Require Import rt.restructuring.model.preemption.rtc_threshold.instance.limited.
diff --git a/restructuring/analysis/basic_facts/preemption/rtc_threshold/nonpreemptive.v b/restructuring/analysis/basic_facts/preemption/rtc_threshold/nonpreemptive.v
index 52153acc98bdfa7e8fab13305edcc69e3362d92b..31307deb5088ec4ea1977d9e9134383a0042da7b 100644
--- a/restructuring/analysis/basic_facts/preemption/rtc_threshold/nonpreemptive.v
+++ b/restructuring/analysis/basic_facts/preemption/rtc_threshold/nonpreemptive.v
@@ -5,7 +5,7 @@ Require Import rt.restructuring.model.task.concept.
 Require Import rt.restructuring.model.schedule.nonpreemptive.
 Require Import rt.restructuring.model.preemption.valid_model.
 Require Import rt.restructuring.model.preemption.job.parameters.
-Require Import rt.restructuring.model.preemption.task.parameters.
+Require Import rt.restructuring.model.task.preemption.parameters.
 Require Import rt.restructuring.model.preemption.rtc_threshold.valid_rtct.
 Require Import rt.restructuring.model.preemption.job.instance.nonpreemptive.
 Require Import rt.restructuring.model.preemption.task.instance.nonpreemptive.
diff --git a/restructuring/analysis/basic_facts/preemption/task/floating.v b/restructuring/analysis/basic_facts/preemption/task/floating.v
index 70284babe480d0feb0002142b85b288af5f10a6d..535c7bcbd473069b46222fb7cae4d58b5e188a0c 100644
--- a/restructuring/analysis/basic_facts/preemption/task/floating.v
+++ b/restructuring/analysis/basic_facts/preemption/task/floating.v
@@ -5,7 +5,7 @@ Require Import rt.restructuring.analysis.definitions.job_properties.
 Require Import rt.restructuring.model.task.concept.
 Require Import rt.restructuring.model.preemption.valid_model.
 Require Import rt.restructuring.model.preemption.job.parameters.
-Require Import rt.restructuring.model.preemption.task.parameters.
+Require Import rt.restructuring.model.task.preemption.parameters.
 Require Import rt.restructuring.model.preemption.rtc_threshold.valid_rtct.
 Require Import rt.restructuring.model.preemption.job.instance.limited.
 Require Import rt.restructuring.model.preemption.valid_schedule.
diff --git a/restructuring/analysis/basic_facts/preemption/task/limited.v b/restructuring/analysis/basic_facts/preemption/task/limited.v
index 7aca2dc6190477fd4e08124ef290deb82b84a774..4851f4076eedd991573c18a2337fd8c92cb9de70 100644
--- a/restructuring/analysis/basic_facts/preemption/task/limited.v
+++ b/restructuring/analysis/basic_facts/preemption/task/limited.v
@@ -5,7 +5,7 @@ Require Import rt.restructuring.analysis.definitions.job_properties.
 Require Import rt.restructuring.model.task.concept.
 Require Import rt.restructuring.model.preemption.valid_model.
 Require Import rt.restructuring.model.preemption.job.parameters.
-Require Import rt.restructuring.model.preemption.task.parameters.
+Require Import rt.restructuring.model.task.preemption.parameters.
 Require Import rt.restructuring.model.preemption.valid_schedule.
 Require Import rt.restructuring.model.preemption.job.instance.limited.
 Require Import rt.restructuring.model.preemption.task.instance.limited.
diff --git a/restructuring/analysis/edf/rta/nonpr_reg/response_time_bound.v b/restructuring/analysis/edf/rta/nonpr_reg/response_time_bound.v
index ccb737e69438aa4563f52823f40deec1db43b243..d24bcd4edb956d3dbd5a3f37d0802cad23a64961 100644
--- a/restructuring/analysis/edf/rta/nonpr_reg/response_time_bound.v
+++ b/restructuring/analysis/edf/rta/nonpr_reg/response_time_bound.v
@@ -9,7 +9,7 @@ Require Import rt.restructuring.model.readiness.basic.
 Require Import rt.restructuring.model.arrival.arrival_curves.
 Require Import rt.restructuring.model.preemption.valid_model.
 Require Import rt.restructuring.model.preemption.job.parameters.
-Require Import rt.restructuring.model.preemption.task.parameters.
+Require Import rt.restructuring.model.task.preemption.parameters.
 Require Import rt.restructuring.model.preemption.rtc_threshold.valid_rtct.
 Require Import rt.restructuring.analysis.basic_facts.preemption.rtc_threshold.job_preemptable.
 Require Import rt.restructuring.analysis.facts.priority_inversion_is_bounded.
diff --git a/restructuring/analysis/edf/rta/response_time_bound.v b/restructuring/analysis/edf/rta/response_time_bound.v
index 931ed0aa6b6d09b2545f03003972fbc320661137..23f6787d0687fad6efbc08d7200e433705f29e84 100644
--- a/restructuring/analysis/edf/rta/response_time_bound.v
+++ b/restructuring/analysis/edf/rta/response_time_bound.v
@@ -10,7 +10,7 @@ Require Import rt.restructuring.model.aggregate.task_arrivals.
 Require Import rt.restructuring.model.arrival.arrival_curves.
 Require Import rt.restructuring.model.preemption.valid_model.
 Require Import rt.restructuring.model.preemption.job.parameters.
-Require Import rt.restructuring.model.preemption.task.parameters.
+Require Import rt.restructuring.model.task.preemption.parameters.
 Require Import rt.restructuring.model.preemption.rtc_threshold.valid_rtct.
 Require Import rt.restructuring.analysis.basic_facts.preemption.rtc_threshold.job_preemptable.
 Require Import rt.restructuring.model.schedule.work_conserving.
diff --git a/restructuring/analysis/facts/priority_inversion_is_bounded.v b/restructuring/analysis/facts/priority_inversion_is_bounded.v
index d552b4ec31e06a708a4300a604454f8f10367a76..ad9688c9f2e696d03dc527933376793c4f781400 100644
--- a/restructuring/analysis/facts/priority_inversion_is_bounded.v
+++ b/restructuring/analysis/facts/priority_inversion_is_bounded.v
@@ -4,7 +4,7 @@ Require Import rt.restructuring.analysis.basic_facts.all.
 Require Import rt.restructuring.model.preemption.valid_model.
 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.task.preemption.parameters.
 Require Import rt.restructuring.model.schedule.priority_driven.
 Require Export rt.restructuring.analysis.definitions.no_carry_in.
 Require Export rt.restructuring.analysis.definitions.busy_interval.
diff --git a/restructuring/analysis/fixed_priority/rta/nonpr_reg/response_time_bound.v b/restructuring/analysis/fixed_priority/rta/nonpr_reg/response_time_bound.v
index 85d7f787894ad56c9bdbfd5d7feacbd8cee72c21..54e45fcc7da41d2c26b3581d8a27c5d500614ce8 100644
--- a/restructuring/analysis/fixed_priority/rta/nonpr_reg/response_time_bound.v
+++ b/restructuring/analysis/fixed_priority/rta/nonpr_reg/response_time_bound.v
@@ -9,7 +9,7 @@ Require Import rt.restructuring.model.readiness.basic.
 Require Import rt.restructuring.model.arrival.arrival_curves.
 Require Import rt.restructuring.model.preemption.valid_model.
 Require Import rt.restructuring.model.preemption.job.parameters.
-Require Import rt.restructuring.model.preemption.task.parameters.
+Require Import rt.restructuring.model.task.preemption.parameters.
 Require Import rt.restructuring.model.preemption.rtc_threshold.valid_rtct.
 Require Import rt.restructuring.model.schedule.work_conserving.
 Require Import rt.restructuring.model.priority.classes.
diff --git a/restructuring/analysis/fixed_priority/rta/response_time_bound.v b/restructuring/analysis/fixed_priority/rta/response_time_bound.v
index 18e460ccd13cf99b483c8f59006ef077857bf362..b80e1ae55ba2ac699bc79b05c007f87181c8e085 100644
--- a/restructuring/analysis/fixed_priority/rta/response_time_bound.v
+++ b/restructuring/analysis/fixed_priority/rta/response_time_bound.v
@@ -9,7 +9,7 @@ Require Import rt.restructuring.model.readiness.basic.
 Require Import rt.restructuring.model.arrival.arrival_curves.
 Require Import rt.restructuring.model.preemption.valid_model.
 Require Import rt.restructuring.model.preemption.job.parameters.
-Require Import rt.restructuring.model.preemption.task.parameters.
+Require Import rt.restructuring.model.task.preemption.parameters.
 Require Import rt.restructuring.model.preemption.rtc_threshold.valid_rtct.
 Require Import rt.restructuring.model.schedule.work_conserving.
 Require Import rt.restructuring.model.priority.classes.
diff --git a/restructuring/model/preemption/job/instance/limited.v b/restructuring/model/preemption/job/instance/limited.v
index d6c3ce92c5d032237c1db1bf017c43a84ab767ce..8b631a17f69a9ec6c277c0636e0b4dcfe5a083b2 100644
--- a/restructuring/model/preemption/job/instance/limited.v
+++ b/restructuring/model/preemption/job/instance/limited.v
@@ -1,5 +1,5 @@
 Require Export rt.restructuring.model.preemption.job.parameters.
-Require Export rt.restructuring.model.preemption.task.parameters.
+Require Export rt.restructuring.model.task.preemption.parameters.
 
 (** Definition of a parameter relating a job
     to the sequence of its preemption points. *)
diff --git a/restructuring/model/preemption/rtc_threshold/instance/floating.v b/restructuring/model/preemption/rtc_threshold/instance/floating.v
index 5197b1e4240acf6f9e53faf66322c827ba5b02cf..4b87a208c04035e13e06dc14e245b23f9c82f873 100644
--- a/restructuring/model/preemption/rtc_threshold/instance/floating.v
+++ b/restructuring/model/preemption/rtc_threshold/instance/floating.v
@@ -1,4 +1,4 @@
-Require Export rt.restructuring.model.preemption.task.parameters.
+Require Export rt.restructuring.model.task.preemption.parameters.
 
 (** * Task's Run to Completion Threshold *)
 (** In this section, we instantiate function [task run to completion
diff --git a/restructuring/model/preemption/rtc_threshold/instance/limited.v b/restructuring/model/preemption/rtc_threshold/instance/limited.v
index c8aa1d8f6cf1ee073933b4c9f8b99b626d246ef4..14efa28707e6b94e6978682dc3b66389fe9bd0dc 100644
--- a/restructuring/model/preemption/rtc_threshold/instance/limited.v
+++ b/restructuring/model/preemption/rtc_threshold/instance/limited.v
@@ -1,4 +1,4 @@
-Require Export rt.restructuring.model.preemption.task.parameters.
+Require Export rt.restructuring.model.task.preemption.parameters.
 
 (** * Task's Run to Completion Threshold *)
 (** In this section, we instantiate function [task run to completion
diff --git a/restructuring/model/preemption/rtc_threshold/instance/nonpreemptive.v b/restructuring/model/preemption/rtc_threshold/instance/nonpreemptive.v
index cb323af10fb7141296875c3947b7867444cf8b53..271f11b4a0ed65f422ca38898634a53d512874ed 100644
--- a/restructuring/model/preemption/rtc_threshold/instance/nonpreemptive.v
+++ b/restructuring/model/preemption/rtc_threshold/instance/nonpreemptive.v
@@ -1,4 +1,4 @@
-Require Export rt.restructuring.model.preemption.task.parameters.
+Require Export rt.restructuring.model.task.preemption.parameters.
 
 From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.
 
diff --git a/restructuring/model/preemption/rtc_threshold/instance/preemptive.v b/restructuring/model/preemption/rtc_threshold/instance/preemptive.v
index cf32a1b91a9bf20c913889c7e728816461261272..30459d065514b25314e78921d5873baade82ef03 100644
--- a/restructuring/model/preemption/rtc_threshold/instance/preemptive.v
+++ b/restructuring/model/preemption/rtc_threshold/instance/preemptive.v
@@ -1,4 +1,4 @@
-Require Export rt.restructuring.model.preemption.task.parameters.
+Require Export rt.restructuring.model.task.preemption.parameters.
 
 (** * Task's Run to Completion Threshold *)
 (** In this section, we instantiate function [task run to completion
diff --git a/restructuring/model/preemption/valid_model.v b/restructuring/model/preemption/valid_model.v
index 5a0299026f5fdf59a9faf5ec0b730896ffeeb2a4..d57aa0543eb8e10f4a9f0d5a10047ba66a36500b 100644
--- a/restructuring/model/preemption/valid_model.v
+++ b/restructuring/model/preemption/valid_model.v
@@ -1,5 +1,5 @@
 Require Export rt.restructuring.model.preemption.job.parameters.
-Require Export rt.restructuring.model.preemption.task.parameters.
+Require Export rt.restructuring.model.task.preemption.parameters.
 
 (** * Platform with limited preemptions *)
 (** Since the notion of preemption points is based on an user-provided 
diff --git a/restructuring/model/preemption/task/parameters.v b/restructuring/model/task/preemption/parameters.v
similarity index 100%
rename from restructuring/model/preemption/task/parameters.v
rename to restructuring/model/task/preemption/parameters.v