diff --git a/restructuring/analysis/basic_facts/preemption/job/limited.v b/restructuring/analysis/basic_facts/preemption/job/limited.v
index 81e57d5753e230ac56cf15a39ab2b50f16c06098..392482c93f18d6973b3d99fb3511379dd6420959 100644
--- a/restructuring/analysis/basic_facts/preemption/job/limited.v
+++ b/restructuring/analysis/basic_facts/preemption/job/limited.v
@@ -2,7 +2,7 @@ Require Export rt.restructuring.analysis.basic_facts.all.
 Require Export rt.restructuring.analysis.definitions.job_properties.
 Require Export rt.restructuring.model.schedule.limited_preemptive.
 
-Require Export rt.restructuring.model.preemption.limited_preemptive.
+Require Import rt.restructuring.model.preemption.limited_preemptive.
 
 (** * Platform for Models with Limited Preemptions *)
 (** In this section, we prove that instantiation of predicate
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 1d05d354e041149a613dfad6da830bb2f4509939..0fd62e5c47e77750ffc69332bc01b29e7f890a97 100644
--- a/restructuring/analysis/edf/rta/nonpr_reg/concrete_models/floating.v
+++ b/restructuring/analysis/edf/rta/nonpr_reg/concrete_models/floating.v
@@ -1,8 +1,10 @@
 Require Export rt.restructuring.analysis.edf.rta.nonpr_reg.response_time_bound.
 Require Export rt.restructuring.analysis.basic_facts.preemption.rtc_threshold.floating.
+Require Import rt.restructuring.model.priority.edf.
 
 Require Import rt.restructuring.model.processor.ideal.
 Require Import rt.restructuring.model.readiness.basic.
+Require Import rt.restructuring.model.preemption.limited_preemptive.
 Require Import rt.restructuring.model.task.preemption.floating_nonpreemptive.
 
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
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 5f3aafd5227e4fa0a45fd6a259e8465db6c3bd22..b7550071d82f68e1b7a3a7d724729da9373a0395 100644
--- a/restructuring/analysis/edf/rta/nonpr_reg/concrete_models/limited.v
+++ b/restructuring/analysis/edf/rta/nonpr_reg/concrete_models/limited.v
@@ -1,8 +1,10 @@
 Require Export rt.restructuring.analysis.edf.rta.nonpr_reg.response_time_bound.
 Require Export rt.restructuring.analysis.basic_facts.preemption.rtc_threshold.limited.
+Require Import rt.restructuring.model.priority.edf.
 
 Require Import rt.restructuring.model.processor.ideal.
 Require Import rt.restructuring.model.readiness.basic.
+Require Import rt.restructuring.model.preemption.limited_preemptive.
 Require Import rt.restructuring.model.task.preemption.limited_preemptive.
 
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
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 503ea76a0fecb947266d67966adfc6463b7ddc84..725cc69ac9be2209d886a07f272c2ef1b042299b 100644
--- a/restructuring/analysis/edf/rta/nonpr_reg/concrete_models/nonpreemptive.v
+++ b/restructuring/analysis/edf/rta/nonpr_reg/concrete_models/nonpreemptive.v
@@ -4,6 +4,7 @@ Require Import rt.restructuring.model.readiness.basic.
 Require Export rt.restructuring.analysis.edf.rta.nonpr_reg.response_time_bound.
 Require Export rt.restructuring.analysis.basic_facts.preemption.task.nonpreemptive.
 Require Export rt.restructuring.analysis.basic_facts.preemption.rtc_threshold.nonpreemptive.
+Require Import rt.restructuring.model.priority.edf.
 
 (** Assume we have a fully non-preemptive model. *)
 Require Import rt.restructuring.model.task.preemption.fully_nonpreemptive.
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 338deb12070711cebd62d9f6d8372d59b2e6df56..6197685dcf250271b45c992264871f77f3170a8f 100644
--- a/restructuring/analysis/edf/rta/nonpr_reg/concrete_models/preemptive.v
+++ b/restructuring/analysis/edf/rta/nonpr_reg/concrete_models/preemptive.v
@@ -4,6 +4,7 @@ Require Import rt.restructuring.model.readiness.basic.
 Require Import rt.restructuring.analysis.edf.rta.nonpr_reg.response_time_bound.
 Require Export rt.restructuring.analysis.basic_facts.preemption.task.preemptive.
 Require Export rt.restructuring.analysis.basic_facts.preemption.rtc_threshold.preemptive.
+Require Import rt.restructuring.model.priority.edf.
 
 (** Assume we have a fully preemptive model. *)
 Require Import rt.restructuring.model.task.preemption.fully_preemptive.
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 de5919d6490f2e30f64607221fc8e8c0d4c57c7a..885eb5881013611b6f3b2456f0f00dd2da098939 100644
--- a/restructuring/analysis/edf/rta/nonpr_reg/response_time_bound.v
+++ b/restructuring/analysis/edf/rta/nonpr_reg/response_time_bound.v
@@ -1,6 +1,7 @@
 Require Export rt.restructuring.analysis.facts.priority_inversion_is_bounded.
 Require Export rt.restructuring.analysis.edf.rta.response_time_bound.
 Require Export rt.restructuring.analysis.arrival.rbf.
+Require Import rt.restructuring.model.priority.edf.
 
 Require Import rt.restructuring.model.processor.ideal.
 Require Import rt.restructuring.model.readiness.basic.
diff --git a/restructuring/analysis/edf/rta/response_time_bound.v b/restructuring/analysis/edf/rta/response_time_bound.v
index 5d71602be938e18d289cc95877d4b8c75fe1bc82..982e050af1353483598a267d7b72a9370b1ac911 100644
--- a/restructuring/analysis/edf/rta/response_time_bound.v
+++ b/restructuring/analysis/edf/rta/response_time_bound.v
@@ -2,6 +2,8 @@ Require Export rt.restructuring.analysis.facts.edf.
 Require Export rt.restructuring.model.schedule.priority_driven.
 Require Export rt.restructuring.analysis.facts.no_carry_in_exists.
 Require Export rt.restructuring.analysis.schedulability.
+Require Import rt.restructuring.model.priority.edf.
+Require Import rt.restructuring.model.task.absolute_deadline.
 
 Require Import rt.restructuring.model.processor.ideal.
 Require Import rt.restructuring.model.readiness.basic.
diff --git a/restructuring/analysis/facts/edf.v b/restructuring/analysis/facts/edf.v
index f9feba174d917a81e375ef6c7d73368ade8bc4df..10cd3dc4c16d716afe190685a0a8283de2bcce8e 100644
--- a/restructuring/analysis/facts/edf.v
+++ b/restructuring/analysis/facts/edf.v
@@ -1,5 +1,5 @@
-Require Export rt.restructuring.model.priority.edf.
-Require Export rt.restructuring.model.task.absolute_deadline.
+Require Import rt.restructuring.model.priority.edf.
+Require Import rt.restructuring.model.task.absolute_deadline.
 
 (** In this section, we prove a few properties about EDF policy. *)
 Section PropertiesOfEDF.
diff --git a/restructuring/analysis/facts/priority_inversion_is_bounded.v b/restructuring/analysis/facts/priority_inversion_is_bounded.v
index 33fa5cd7a4a3668e17668c45a198f3ddb0f6e22b..93c89d784982f9741f7c725455da8da15f224f94 100644
--- a/restructuring/analysis/facts/priority_inversion_is_bounded.v
+++ b/restructuring/analysis/facts/priority_inversion_is_bounded.v
@@ -3,6 +3,9 @@ Require Export rt.restructuring.model.schedule.priority_driven.
 Require Export rt.restructuring.analysis.facts.no_carry_in_exists.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
 
+(** Throughout this file, we assume ideal uniprocessor schedules. *)
+Require Import rt.restructuring.model.processor.ideal.
+
 (** Throughout the file we assume for the classic Liu & Layland model
     of readiness without jitter and no self-suspensions, where
     pending jobs are always ready. *)
diff --git a/restructuring/analysis/facts/readiness/basic.v b/restructuring/analysis/facts/readiness/basic.v
index 5875f85465699dad12b4e0aa99580c560976faad..c10e406bb5320b6f51eb5635aee3c80d6edd2799 100644
--- a/restructuring/analysis/facts/readiness/basic.v
+++ b/restructuring/analysis/facts/readiness/basic.v
@@ -1,6 +1,8 @@
-Require Export rt.restructuring.model.readiness.basic.
 Require Import rt.restructuring.analysis.basic_facts.completion.
 
+(** Throughout this file, we assume the basic (i.e., Liu & Layland) readiness model. *)
+Require Import rt.restructuring.model.readiness.basic.
+
 Section LiuAndLaylandReadiness.
   (** Consider any kind of jobs... *)
   Context {Job : JobType}.
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 988413f76256ab7e6ed358081038846d8bc55bb3..18e002d13381c7177f5818ee4b124eb11709c12d 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
@@ -7,6 +7,7 @@ Require Import rt.restructuring.model.processor.ideal.
 (** Throughout this file, we assume the basic (i.e., Liu & Layland) readiness model. *)
 Require Import rt.restructuring.model.readiness.basic.
 
+Require Import rt.restructuring.model.preemption.limited_preemptive.
 Require Import rt.restructuring.model.task.preemption.floating_nonpreemptive.
 
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
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 214f3969633db03c24ebc1bf4ce42f3130357762..099c7bf599a2130c874f879ddf38c84e215e508a 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
@@ -7,6 +7,7 @@ Require Import rt.restructuring.model.processor.ideal.
 (** Throughout this file, we assume the basic (i.e., Liu & Layland) readiness model. *)
 Require Import rt.restructuring.model.readiness.basic.
 
+Require Import rt.restructuring.model.preemption.limited_preemptive.
 Require Import rt.restructuring.model.task.preemption.limited_preemptive.
 
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
diff --git a/restructuring/analysis/schedulability.v b/restructuring/analysis/schedulability.v
index 9c0bd70fc06f2cfd8881e31866b2a314015dfe3c..a3de0ced0c3dbcffad206ca9174b477b1a5bf2ef 100644
--- a/restructuring/analysis/schedulability.v
+++ b/restructuring/analysis/schedulability.v
@@ -1,5 +1,5 @@
-Require Export rt.restructuring.model.task.absolute_deadline.
 Require Export rt.restructuring.analysis.basic_facts.completion.
+Require Import rt.restructuring.model.task.absolute_deadline.
 
 Section Task.
   Context {Task : TaskType}.
diff --git a/restructuring/model/schedule/limited_preemptive.v b/restructuring/model/schedule/limited_preemptive.v
index 2cc39396f778f9c3346ddeb7b2f78085ee3da2b6..a69d30dc6973a13b76ca42bf0f711f9b09c40edb 100644
--- a/restructuring/model/schedule/limited_preemptive.v
+++ b/restructuring/model/schedule/limited_preemptive.v
@@ -1,8 +1,9 @@
-Require Export rt.restructuring.model.processor.ideal.
-Require Export rt.restructuring.model.preemption.parameter.
- 
+Require Export rt.restructuring.model.preemption.parameter. 
 From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.
 
+(** Throughout this file, we assume ideal uniprocessor schedules. *)
+Require Import rt.restructuring.model.processor.ideal.
+
 (** * Schedule with Limited Preemptions *)
 (** In this section we introduce the notion of preemptions-aware
     schedule. *)
diff --git a/restructuring/model/schedule/preemption_time.v b/restructuring/model/schedule/preemption_time.v
index 790fd66f77cf0f939b868ae41bd079b6b1b8421e..df873a28503046f5c1ea44731b92c7c82bc65a29 100644
--- a/restructuring/model/schedule/preemption_time.v
+++ b/restructuring/model/schedule/preemption_time.v
@@ -1,7 +1,9 @@
-Require Export rt.restructuring.model.processor.ideal.
 Require Export rt.restructuring.model.preemption.parameter.
 From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.
 
+(** Throughout this file, we assume ideal uniprocessor schedules. *)
+Require Import rt.restructuring.model.processor.ideal.
+
 (** * Preemption Time in Ideal Uni-Processor Model *)
 (** In this section we define the notion of preemption _time_ for
     ideal uni-processor model. *)
diff --git a/restructuring/model/schedule/tdma.v b/restructuring/model/schedule/tdma.v
index 7b32d2dbc94871cab7f10a35c0dc89944cbe0f1c..6175d3d009a4f407253aaa18485e434f5bdf9e82 100644
--- a/restructuring/model/schedule/tdma.v
+++ b/restructuring/model/schedule/tdma.v
@@ -1,9 +1,11 @@
 Require Export rt.restructuring.model.task.concept.
-Require Export rt.restructuring.model.processor.ideal.
 Require Export rt.util.seqset.
 Require Export rt.util.rel.
 From mathcomp Require Export ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop div.
 
+(** Throughout this file, we assume ideal uniprocessor schedules. *)
+Require Import rt.restructuring.model.processor.ideal.
+
 (** In this section, we define the TDMA policy.*)
 Section TDMAPolicy.
 
diff --git a/restructuring/model/task/preemption/limited_preemptive.v b/restructuring/model/task/preemption/limited_preemptive.v
index aa33cabcaff2c0a9f35b8fae910fcf7a2eca2e3b..5b6b7f687457ea382e8cb9ad9f4d58b3e0c66b44 100644
--- a/restructuring/model/task/preemption/limited_preemptive.v
+++ b/restructuring/model/task/preemption/limited_preemptive.v
@@ -1,8 +1,8 @@
-Require Export rt.restructuring.model.preemption.limited_preemptive.
 Require Export rt.restructuring.model.task.preemption.parameters.
-
 From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.
 
+Require Import rt.restructuring.model.preemption.limited_preemptive.
+
 (** * Platform for Models with Limited Preemptions *)
 (** In this section, we introduce a set of requirements for function
     [task_preemption_points], so it is coherent with limited