diff --git a/restructuring/analysis/transform/edf_trans.v b/restructuring/analysis/transform/edf_trans.v
index 210d7675c51f5455d7cbc2c608913a08a443ba17..65ed0841bbd98429c2427a858d6e3320796a463f 100644
--- a/restructuring/analysis/transform/edf_trans.v
+++ b/restructuring/analysis/transform/edf_trans.v
@@ -1,6 +1,5 @@
 Require Export rt.restructuring.analysis.transform.prefix.
 Require Export rt.restructuring.analysis.transform.swap.
-Require Export rt.util.search_arg.
 
 (** In this file we define the "EDF-ification" of a schedule, the
     operation at the core of the EDF optimality proof. *)
diff --git a/restructuring/analysis/transform/facts/edf_opt.v b/restructuring/analysis/transform/facts/edf_opt.v
index db2e81b48bc01751359607927dcd216a9be1f41c..1be7c88f964b2e54d5db8d7739cfdd017f971f1c 100644
--- a/restructuring/analysis/transform/facts/edf_opt.v
+++ b/restructuring/analysis/transform/facts/edf_opt.v
@@ -1,14 +1,10 @@
 From mathcomp Require Import ssrnat ssrbool fintype.
-Require Export rt.restructuring.analysis.basic_facts.all.
 Require Export rt.restructuring.model.schedule.edf.
 Require Export rt.restructuring.analysis.schedulability.
 Require Export rt.restructuring.analysis.transform.edf_trans.
 Require Export rt.restructuring.analysis.transform.facts.swaps.
 Require Export rt.restructuring.analysis.facts.readiness.basic.
 
-Require Import rt.util.tactics.
-Require Import rt.util.nat.
-
 (** This file contains the main argument of the EDF optimality proof,
     starting with an analysis of the individual functions that drive
     the "EDF-ication" of a given reference schedule and ending with
diff --git a/restructuring/analysis/transform/facts/replace_at.v b/restructuring/analysis/transform/facts/replace_at.v
index 9b0f7ed3fbfe996d3c462fd04abbe6124bdebcfe..5e22b2dfee24d5e0db8587a0225502aaa6f591de 100644
--- a/restructuring/analysis/transform/facts/replace_at.v
+++ b/restructuring/analysis/transform/facts/replace_at.v
@@ -1,6 +1,4 @@
 Require Export rt.restructuring.analysis.transform.swap.
-Require Import rt.restructuring.analysis.basic_facts.all.
-Require Import rt.util.nat.
 
 (** In this file, we make a few simple observations about schedules with
     replacements. *)
diff --git a/restructuring/analysis/transform/prefix.v b/restructuring/analysis/transform/prefix.v
index d7fd08aa12df1a25c891e63e768f0ccea0ef1cc7..288b202d8884478db2adc3b95715834e6c575a96 100644
--- a/restructuring/analysis/transform/prefix.v
+++ b/restructuring/analysis/transform/prefix.v
@@ -1,6 +1,5 @@
 From mathcomp Require Import ssrnat ssrbool fintype.
-Require Export rt.restructuring.behavior.all.
-Require Import rt.restructuring.analysis.basic_facts.all.
+Require Export rt.restructuring.analysis.basic_facts.all.
 
 (** This file provides an operation that transforms a finite prefix of
     a given schedule by applying a point-wise transformation to each
diff --git a/restructuring/analysis/transform/swap.v b/restructuring/analysis/transform/swap.v
index 0ffa025027b26c6fc47b493c3c57c7540089ac20..96dc092d24c9975ebfb64cb766ba76749ec20296 100644
--- a/restructuring/analysis/transform/swap.v
+++ b/restructuring/analysis/transform/swap.v
@@ -1,5 +1,4 @@
-Require Export rt.restructuring.behavior.all.
-Require Import rt.restructuring.analysis.basic_facts.all.
+Require Export rt.restructuring.analysis.basic_facts.all.
 
 (** This file defines simple allocation substitutions and a swapping operation
     as used for instance in the classic EDF optimality proof. *)