diff --git a/restructuring/model/preemption/limited_preemptive.v b/restructuring/model/preemption/limited_preemptive.v
index d4345918c966c593b041f9b017c133a413985773..9af1016a5c23a7f14b20939b7e8946355086b54b 100644
--- a/restructuring/model/preemption/limited_preemptive.v
+++ b/restructuring/model/preemption/limited_preemptive.v
@@ -1,5 +1,4 @@
 Require Export rt.restructuring.model.preemption.parameter.
-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/task/preemption/floating_nonpreemptive.v b/restructuring/model/task/preemption/floating_nonpreemptive.v
index d0e75b0ac27f5734022b05d7938790db909b8545..a66d11cc539fae00f8e3c794b2a39d9ea244a5a5 100644
--- a/restructuring/model/task/preemption/floating_nonpreemptive.v
+++ b/restructuring/model/task/preemption/floating_nonpreemptive.v
@@ -1,4 +1,5 @@
 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.
 
diff --git a/restructuring/model/task/preemption/limited_preemptive.v b/restructuring/model/task/preemption/limited_preemptive.v
index 343a6db764f32b60d2d7bebf77987f1900587e41..aa33cabcaff2c0a9f35b8fae910fcf7a2eca2e3b 100644
--- a/restructuring/model/task/preemption/limited_preemptive.v
+++ b/restructuring/model/task/preemption/limited_preemptive.v
@@ -1,4 +1,5 @@
 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.