diff --git a/restructuring/analysis/abstract/instantiations/ideal_processor.v b/restructuring/analysis/abstract/instantiations/ideal_processor.v
index e57014b413a16f8a67137089775f41bcdbcaf0c0..69f89f25eb5fd431d4ca8f3f999ae5bf47aac36a 100644
--- a/restructuring/analysis/abstract/instantiations/ideal_processor.v
+++ b/restructuring/analysis/abstract/instantiations/ideal_processor.v
@@ -3,7 +3,7 @@ Require Export rt.restructuring.model.task.
 Require Export rt.restructuring.model.aggregate.workload.
 Require Import rt.restructuring.model.schedule.work_conserving.
 Require Import rt.restructuring.model.schedule.sequential.
-Require Import rt.restructuring.model.schedule.priority_based.priorities.
+Require Import rt.restructuring.model.priority.classes.
 Require Import rt.restructuring.analysis.definitions.busy_interval.
 Require Import rt.restructuring.analysis.definitions.priority_inversion.
 Require Import rt.restructuring.analysis.abstract.core.definitions.
diff --git a/restructuring/analysis/arrival/workload_bound.v b/restructuring/analysis/arrival/workload_bound.v
index 70798f72da6d364c6842b28477c647951cd5f953..bdb5ba43e4018528842cb91852c1a2ce48ed53fb 100644
--- a/restructuring/analysis/arrival/workload_bound.v
+++ b/restructuring/analysis/arrival/workload_bound.v
@@ -1,7 +1,7 @@
 Require Import rt.util.sum.
 Require Export rt.restructuring.behavior.all.
 Require Import rt.restructuring.model.task.
-Require Import rt.restructuring.model.schedule.priority_based.priorities.
+Require Import rt.restructuring.model.priority.classes.
 Require Import rt.restructuring.model.aggregate.task_arrivals.
 Require Import rt.restructuring.model.arrival.arrival_curves.
 Require Import rt.restructuring.analysis.basic_facts.workload.
diff --git a/restructuring/analysis/basic_facts/service_of_jobs.v b/restructuring/analysis/basic_facts/service_of_jobs.v
index 20f6070655f339f88be5602b0990e204f062afea..93741e6f15b62f50c0d5d84caf831a94dd626aca 100644
--- a/restructuring/analysis/basic_facts/service_of_jobs.v
+++ b/restructuring/analysis/basic_facts/service_of_jobs.v
@@ -6,7 +6,7 @@ Require Export rt.restructuring.model.aggregate.workload.
 Require Export rt.restructuring.model.aggregate.service_of_jobs.
 Require Export rt.restructuring.model.processor.ideal.
 Require Export rt.restructuring.model.processor.platform_properties.
-Require Import rt.restructuring.model.schedule.priority_based.priorities.
+Require Import rt.restructuring.model.priority.classes.
 
 Require Import rt.restructuring.analysis.basic_facts.arrivals.
 Require Import rt.restructuring.analysis.basic_facts.service.
diff --git a/restructuring/analysis/basic_facts/workload.v b/restructuring/analysis/basic_facts/workload.v
index a049cb0042721a4254eecaf67c8b05e087e7cb2c..67c71814b7cfc8f3edbbda7b804e82deb2ded405 100644
--- a/restructuring/analysis/basic_facts/workload.v
+++ b/restructuring/analysis/basic_facts/workload.v
@@ -1,6 +1,6 @@
 Require Export rt.restructuring.behavior.all.
 Require Export rt.restructuring.model.aggregate.workload.
-Require Export rt.restructuring.model.schedule.priority_based.priorities.
+Require Export rt.restructuring.model.priority.classes.
 Require Import rt.restructuring.analysis.basic_facts.arrivals.
 
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
diff --git a/restructuring/analysis/definitions/priority_inversion.v b/restructuring/analysis/definitions/priority_inversion.v
index f0367af97d34fa3f0dd905d2fd23c49c186d55a6..076db9e0915e2182a3fee853df1d360f7c92ab10 100644
--- a/restructuring/analysis/definitions/priority_inversion.v
+++ b/restructuring/analysis/definitions/priority_inversion.v
@@ -4,7 +4,7 @@ Require Export rt.restructuring.analysis.basic_facts.all.
 Require Export rt.restructuring.model.job.
 Require Export rt.restructuring.model.task.
 Require Export rt.restructuring.model.schedule.work_conserving.
-Require Export rt.restructuring.model.schedule.priority_based.priorities.
+Require Export rt.restructuring.model.priority.classes.
 Require Export rt.restructuring.analysis.definitions.busy_interval.
 
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
diff --git a/restructuring/analysis/edf/rta/nonpr_reg/concrete_models/floating.v b/restructuring/analysis/edf/rta/nonpr_reg/concrete_models/floating.v
index 5185299fab2f265690bb27d3ba41b94ba8412129..d5497e73b02501556040bbeeae1ff75517668133 100644
--- a/restructuring/analysis/edf/rta/nonpr_reg/concrete_models/floating.v
+++ b/restructuring/analysis/edf/rta/nonpr_reg/concrete_models/floating.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.floating.
 Require Import rt.restructuring.model.schedule.work_conserving.
-Require Import rt.restructuring.model.schedule.priority_based.priorities.
+Require Import rt.restructuring.model.priority.classes.
 Require Import rt.restructuring.model.schedule.priority_based.edf.
 Require Import rt.restructuring.model.schedule.priority_based.preemption_aware.
 Require Import rt.restructuring.analysis.arrival.workload_bound.
diff --git a/restructuring/analysis/edf/rta/nonpr_reg/concrete_models/limited.v b/restructuring/analysis/edf/rta/nonpr_reg/concrete_models/limited.v
index 46937e75fa7faea2a66aa8faf2ba81dd33b2c857..0db53dbef04c2df679006a964fa051841d39b5e9 100644
--- a/restructuring/analysis/edf/rta/nonpr_reg/concrete_models/limited.v
+++ b/restructuring/analysis/edf/rta/nonpr_reg/concrete_models/limited.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.limited.
 Require Import rt.restructuring.model.schedule.work_conserving.
-Require Import rt.restructuring.model.schedule.priority_based.priorities.
+Require Import rt.restructuring.model.priority.classes.
 Require Import rt.restructuring.model.schedule.priority_based.edf.
 Require Import rt.restructuring.model.schedule.priority_based.preemption_aware.
 Require Import rt.restructuring.analysis.arrival.workload_bound.
diff --git a/restructuring/analysis/edf/rta/nonpr_reg/concrete_models/nonpreemptive.v b/restructuring/analysis/edf/rta/nonpr_reg/concrete_models/nonpreemptive.v
index c8d39e1e0285cd1749929901dc4fb0d36721ee16..8212144b830d61ec2264747d6e20d464819230f1 100644
--- a/restructuring/analysis/edf/rta/nonpr_reg/concrete_models/nonpreemptive.v
+++ b/restructuring/analysis/edf/rta/nonpr_reg/concrete_models/nonpreemptive.v
@@ -8,7 +8,7 @@ Require Import rt.restructuring.model.processor.ideal.
 Require Import rt.restructuring.model.readiness.basic.
 Require Import rt.restructuring.model.arrival.arrival_curves.
 Require Import rt.restructuring.model.schedule.work_conserving.
-Require Import rt.restructuring.model.schedule.priority_based.priorities.
+Require Import rt.restructuring.model.priority.classes.
 Require Import rt.restructuring.model.schedule.priority_based.edf.
 Require Import rt.restructuring.model.schedule.priority_based.preemption_aware.
 Require Import rt.restructuring.analysis.arrival.workload_bound.
diff --git a/restructuring/analysis/edf/rta/nonpr_reg/concrete_models/preemptive.v b/restructuring/analysis/edf/rta/nonpr_reg/concrete_models/preemptive.v
index 8a73acd952b44027f0b648f2faa8d1b3ae341aa8..04a01e3c4e7ccf04bddb316d4e449fe952b5577f 100644
--- a/restructuring/analysis/edf/rta/nonpr_reg/concrete_models/preemptive.v
+++ b/restructuring/analysis/edf/rta/nonpr_reg/concrete_models/preemptive.v
@@ -8,7 +8,7 @@ Require Import rt.restructuring.model.processor.ideal.
 Require Import rt.restructuring.model.readiness.basic.
 Require Import rt.restructuring.model.arrival.arrival_curves.
 Require Import rt.restructuring.model.schedule.work_conserving.
-Require Import rt.restructuring.model.schedule.priority_based.priorities.
+Require Import rt.restructuring.model.priority.classes.
 Require Import rt.restructuring.model.schedule.priority_based.edf.
 Require Import rt.restructuring.model.schedule.priority_based.preemption_aware.
 Require Import rt.restructuring.analysis.arrival.workload_bound.
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 b6c66b81db7b80cb51fa0cbaf8f7720811a178cb..d266393a6fca83e1ebdabde0112053fc2db7a840 100644
--- a/restructuring/analysis/edf/rta/nonpr_reg/response_time_bound.v
+++ b/restructuring/analysis/edf/rta/nonpr_reg/response_time_bound.v
@@ -14,7 +14,7 @@ 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.
 Require Import rt.restructuring.model.schedule.work_conserving.
-Require Import rt.restructuring.model.schedule.priority_based.priorities.
+Require Import rt.restructuring.model.priority.classes.
 Require Import rt.restructuring.model.schedule.priority_based.edf.
 Require Import rt.restructuring.model.schedule.priority_based.preemption_aware.
 Require Import rt.restructuring.analysis.arrival.workload_bound.
diff --git a/restructuring/analysis/edf/rta/response_time_bound.v b/restructuring/analysis/edf/rta/response_time_bound.v
index f64d965fee00d597354462c94cba967cb5ee09a6..0fbb317ab981cf07afacd41eef03485850e23946 100644
--- a/restructuring/analysis/edf/rta/response_time_bound.v
+++ b/restructuring/analysis/edf/rta/response_time_bound.v
@@ -14,7 +14,7 @@ Require Import rt.restructuring.model.preemption.task.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.
-Require Import rt.restructuring.model.schedule.priority_based.priorities.
+Require Import rt.restructuring.model.priority.classes.
 Require Import rt.restructuring.model.schedule.priority_based.edf.
 Require Import rt.restructuring.model.schedule.priority_based.preemption_aware.
 Require Import rt.restructuring.analysis.arrival.workload_bound.
diff --git a/restructuring/analysis/facts/busy_interval_exists.v b/restructuring/analysis/facts/busy_interval_exists.v
index 0dfdaa5b93e8e5a52cc8d5856dbb444b63fc1b79..4a402cc0551497a53b25636fea4e057253c7e91a 100644
--- a/restructuring/analysis/facts/busy_interval_exists.v
+++ b/restructuring/analysis/facts/busy_interval_exists.v
@@ -4,7 +4,7 @@ Require Export rt.restructuring.analysis.basic_facts.all.
 Require Export rt.restructuring.model.job.
 Require Export rt.restructuring.model.task.
 Require Export rt.restructuring.model.schedule.work_conserving.
-Require Export rt.restructuring.model.schedule.priority_based.priorities.
+Require Export rt.restructuring.model.priority.classes.
 Require Export rt.restructuring.analysis.definitions.busy_interval.
 Require Export rt.restructuring.analysis.definitions.priority_inversion.
 
diff --git a/restructuring/analysis/facts/no_carry_in_exists.v b/restructuring/analysis/facts/no_carry_in_exists.v
index 478de73498d9887015f14c2b0fd2b2f7c2c5c10c..b7aa4490fb37957407b53956ca096f90470d0f21 100644
--- a/restructuring/analysis/facts/no_carry_in_exists.v
+++ b/restructuring/analysis/facts/no_carry_in_exists.v
@@ -4,7 +4,7 @@ Require Export rt.restructuring.analysis.basic_facts.all.
 Require Export rt.restructuring.model.job.
 Require Export rt.restructuring.model.task.
 Require Export rt.restructuring.model.schedule.work_conserving.
-Require Export rt.restructuring.model.schedule.priority_based.priorities.
+Require Export rt.restructuring.model.priority.classes.
 Require Export rt.restructuring.analysis.definitions.no_carry_in.
 Require Export rt.restructuring.analysis.definitions.busy_interval.
 Require Export rt.restructuring.analysis.definitions.priority_inversion.
diff --git a/restructuring/analysis/fixed_priority/rta/nonpr_reg/concrete_models/floating.v b/restructuring/analysis/fixed_priority/rta/nonpr_reg/concrete_models/floating.v
index 9fa2cb467150bda7d8956f46e9ea8a921a99be18..3f15c28b0518254679e5f16777cf714de0c3fc7c 100644
--- a/restructuring/analysis/fixed_priority/rta/nonpr_reg/concrete_models/floating.v
+++ b/restructuring/analysis/fixed_priority/rta/nonpr_reg/concrete_models/floating.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.floating.
 Require Import rt.restructuring.model.schedule.work_conserving.
-Require Import rt.restructuring.model.schedule.priority_based.priorities.
+Require Import rt.restructuring.model.priority.classes.
 Require Import rt.restructuring.model.schedule.priority_based.preemption_aware.
 Require Import rt.restructuring.analysis.arrival.workload_bound.
 Require Import rt.restructuring.analysis.arrival.rbf.
diff --git a/restructuring/analysis/fixed_priority/rta/nonpr_reg/concrete_models/limited.v b/restructuring/analysis/fixed_priority/rta/nonpr_reg/concrete_models/limited.v
index ecf26b2d2d92c355d12236338a0d88ff550a67d2..fe73e59a1a126fdfebdf8480883dfc52a56c4ac5 100644
--- a/restructuring/analysis/fixed_priority/rta/nonpr_reg/concrete_models/limited.v
+++ b/restructuring/analysis/fixed_priority/rta/nonpr_reg/concrete_models/limited.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.limited.
 Require Import rt.restructuring.model.schedule.work_conserving.
-Require Import rt.restructuring.model.schedule.priority_based.priorities.
+Require Import rt.restructuring.model.priority.classes.
 Require Import rt.restructuring.model.schedule.priority_based.preemption_aware.
 Require Import rt.restructuring.analysis.arrival.workload_bound.
 Require Import rt.restructuring.analysis.arrival.rbf.
diff --git a/restructuring/analysis/fixed_priority/rta/nonpr_reg/concrete_models/nonpreemptive.v b/restructuring/analysis/fixed_priority/rta/nonpr_reg/concrete_models/nonpreemptive.v
index fd36a8f6a8fe018ec3bb91ef33ba3024913989dd..78c93cd0645d088a677f8a036a3ece81ee5c6cd9 100644
--- a/restructuring/analysis/fixed_priority/rta/nonpr_reg/concrete_models/nonpreemptive.v
+++ b/restructuring/analysis/fixed_priority/rta/nonpr_reg/concrete_models/nonpreemptive.v
@@ -8,7 +8,7 @@ Require Import rt.restructuring.model.processor.ideal.
 Require Import rt.restructuring.model.readiness.basic.
 Require Import rt.restructuring.model.arrival.arrival_curves.
 Require Import rt.restructuring.model.schedule.work_conserving.
-Require Import rt.restructuring.model.schedule.priority_based.priorities.
+Require Import rt.restructuring.model.priority.classes.
 Require Import rt.restructuring.model.schedule.priority_based.preemption_aware.
 Require Import rt.restructuring.analysis.arrival.workload_bound.
 Require Import rt.restructuring.analysis.arrival.rbf.
diff --git a/restructuring/analysis/fixed_priority/rta/nonpr_reg/concrete_models/preemptive.v b/restructuring/analysis/fixed_priority/rta/nonpr_reg/concrete_models/preemptive.v
index 80b08a0f0fe56a09e9dbd69eca98eb5d9ebcaa19..565952da95d9e2bdd959df561d4556403615af98 100644
--- a/restructuring/analysis/fixed_priority/rta/nonpr_reg/concrete_models/preemptive.v
+++ b/restructuring/analysis/fixed_priority/rta/nonpr_reg/concrete_models/preemptive.v
@@ -8,7 +8,7 @@ Require Import rt.restructuring.model.processor.ideal.
 Require Import rt.restructuring.model.readiness.basic.
 Require Import rt.restructuring.model.arrival.arrival_curves.
 Require Import rt.restructuring.model.schedule.work_conserving.
-Require Import rt.restructuring.model.schedule.priority_based.priorities.
+Require Import rt.restructuring.model.priority.classes.
 Require Import rt.restructuring.model.schedule.priority_based.preemption_aware.
 Require Import rt.restructuring.analysis.arrival.workload_bound.
 Require Import rt.restructuring.analysis.arrival.rbf.
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 d96346587430f90e5c16506f6cbbd6ea14b298fd..1b91e8ccf26e4a6676fab408d7b4417ae33b2e3a 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
@@ -12,7 +12,7 @@ Require Import rt.restructuring.model.preemption.job.parameters.
 Require Import rt.restructuring.model.preemption.task.parameters.
 Require Import rt.restructuring.model.preemption.rtc_threshold.valid_rtct.
 Require Import rt.restructuring.model.schedule.work_conserving.
-Require Import rt.restructuring.model.schedule.priority_based.priorities.
+Require Import rt.restructuring.model.priority.classes.
 Require Import rt.restructuring.model.schedule.priority_based.preemption_aware.
 Require Import rt.restructuring.analysis.arrival.workload_bound.
 Require Import rt.restructuring.analysis.arrival.rbf.
diff --git a/restructuring/analysis/fixed_priority/rta/response_time_bound.v b/restructuring/analysis/fixed_priority/rta/response_time_bound.v
index d086e808297abd075e8592981112906ef9e3a4b1..b1ed59948ef82442590c1d13f562d4e994b2e240 100644
--- a/restructuring/analysis/fixed_priority/rta/response_time_bound.v
+++ b/restructuring/analysis/fixed_priority/rta/response_time_bound.v
@@ -12,7 +12,7 @@ Require Import rt.restructuring.model.preemption.job.parameters.
 Require Import rt.restructuring.model.preemption.task.parameters.
 Require Import rt.restructuring.model.preemption.rtc_threshold.valid_rtct.
 Require Import rt.restructuring.model.schedule.work_conserving.
-Require Import rt.restructuring.model.schedule.priority_based.priorities.
+Require Import rt.restructuring.model.priority.classes.
 Require Import rt.restructuring.model.schedule.priority_based.preemption_aware.
 Require Import rt.restructuring.analysis.arrival.workload_bound.
 Require Import rt.restructuring.analysis.arrival.rbf.
diff --git a/restructuring/model/aggregate/service_of_jobs.v b/restructuring/model/aggregate/service_of_jobs.v
index 2fdd41a5af862dbc50430878c6714758c85a59af..0d6af127644e2f67c687a634b0abf8b472b6a2b1 100644
--- a/restructuring/model/aggregate/service_of_jobs.v
+++ b/restructuring/model/aggregate/service_of_jobs.v
@@ -1,4 +1,4 @@
-Require Export rt.restructuring.model.schedule.priority_based.priorities.
+Require Export rt.restructuring.model.priority.classes.
 Require Export rt.restructuring.model.processor.ideal.
      
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
diff --git a/restructuring/model/aggregate/workload.v b/restructuring/model/aggregate/workload.v
index f7e0b20938296430b761ca7ab4d201fba7563be4..9040dbbcb30af4270b6fb406a45246045da8d625 100644
--- a/restructuring/model/aggregate/workload.v
+++ b/restructuring/model/aggregate/workload.v
@@ -1,4 +1,4 @@
-Require Export rt.restructuring.model.schedule.priority_based.priorities.
+Require Export rt.restructuring.model.priority.classes.
 
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
 
diff --git a/restructuring/model/schedule/priority_based/priorities.v b/restructuring/model/priority/classes.v
similarity index 100%
rename from restructuring/model/schedule/priority_based/priorities.v
rename to restructuring/model/priority/classes.v
diff --git a/restructuring/model/schedule/priority_based/edf.v b/restructuring/model/schedule/priority_based/edf.v
index daaf6ce3fe2f969d3bd577f0f9a1cce797744215..17a8c25904357a90942000d87dcb53087fef5285 100644
--- a/restructuring/model/schedule/priority_based/edf.v
+++ b/restructuring/model/schedule/priority_based/edf.v
@@ -1,5 +1,5 @@
 Require Export rt.restructuring.model.job_deadline.
-Require Import rt.restructuring.model.schedule.priority_based.priorities.
+Require Import rt.restructuring.model.priority.classes.
 From mathcomp Require Export seq.
 
 (** In this section we introduce the notion of EDF priorities. *)
diff --git a/restructuring/model/schedule/priority_based/preemption_aware.v b/restructuring/model/schedule/priority_based/preemption_aware.v
index 3918c457db82234cd01db0b2144bdc7cbd36e4d0..59e8b33d31a58c0dea726e7762db138d94e38965 100644
--- a/restructuring/model/schedule/priority_based/preemption_aware.v
+++ b/restructuring/model/schedule/priority_based/preemption_aware.v
@@ -1,4 +1,4 @@
-Require Export rt.restructuring.model.schedule.priority_based.priorities.
+Require Export rt.restructuring.model.priority.classes.
 Require Export rt.restructuring.model.preemption.preemption_time.
 
 (** We now define what it means for a schedule to respect a priority
diff --git a/restructuring/model/schedule/priority_based/preemptive.v b/restructuring/model/schedule/priority_based/preemptive.v
index fda8599228fb2eb52619841535c88e6eed688def..d41123a36162d9457361287de6f734b8648b4130 100644
--- a/restructuring/model/schedule/priority_based/preemptive.v
+++ b/restructuring/model/schedule/priority_based/preemptive.v
@@ -1,4 +1,4 @@
-Require Export rt.restructuring.model.schedule.priority_based.priorities.
+Require Export rt.restructuring.model.priority.classes.
 
 (** We now define what it means for a schedule to respect a priority *)
 (** We only define it for a JLDP policy since the definitions for JLDP and JLFP are the same