diff --git a/restructuring/analysis/basic_facts/arrivals.v b/restructuring/analysis/basic_facts/arrivals.v
index 3dabfe00d50d59dd85395b85e056fc19daacd36b..a9eb167ab5d8a9c5b2e68f5256628861275bc0e9 100644
--- a/restructuring/analysis/basic_facts/arrivals.v
+++ b/restructuring/analysis/basic_facts/arrivals.v
@@ -1,5 +1,5 @@
 Require Export rt.restructuring.behavior.all.
-Require Import rt.util.all.
+Require Export rt.util.all.
 
 (** In this section, we relate job readiness to [has_arrived]. *)
 Section Arrived.
diff --git a/restructuring/analysis/basic_facts/completion.v b/restructuring/analysis/basic_facts/completion.v
index 53ae48195d910568ad5bed69f620ee00617f2716..d57646ad175a9609ec730b111409767ff5a3cd90 100644
--- a/restructuring/analysis/basic_facts/completion.v
+++ b/restructuring/analysis/basic_facts/completion.v
@@ -2,7 +2,7 @@ Require Export rt.restructuring.behavior.all.
 Require Export rt.restructuring.analysis.basic_facts.service.
 Require Export rt.restructuring.analysis.basic_facts.arrivals.
 
-Require Import rt.util.nat.
+Require Export rt.util.nat.
 
 (** In this file, we establish basic facts about job completions. *)
 
diff --git a/restructuring/analysis/edf/optimality.v b/restructuring/analysis/edf/optimality.v
index 18942ad7b14f22d65615caa0070468c4039aa25c..121c124f0a96fe23384a2c67555036434a0e80fc 100644
--- a/restructuring/analysis/edf/optimality.v
+++ b/restructuring/analysis/edf/optimality.v
@@ -1,6 +1,4 @@
-Require Export rt.restructuring.model.schedule.edf.
-Require Import rt.restructuring.analysis.schedulability.
-Require Import rt.restructuring.analysis.transform.facts.edf_opt.
+Require Export rt.restructuring.analysis.transform.facts.edf_opt.
 
 (** This file contains the theorem that states the famous EDF
     optimality result: if there is any way to meet all deadlines
diff --git a/restructuring/analysis/schedulability.v b/restructuring/analysis/schedulability.v
index 2104ea905b654a6519ee58bfc8e45c54129b291f..ca0048037dca11467777283d7300399e631631a9 100644
--- a/restructuring/analysis/schedulability.v
+++ b/restructuring/analysis/schedulability.v
@@ -1,8 +1,5 @@
-Require Export rt.restructuring.behavior.all.
-Require Export rt.restructuring.model.task.
 Require Export rt.restructuring.model.job_deadline.
 Require Export rt.restructuring.analysis.basic_facts.completion.
-Require Export rt.util.seqset.
 
 Section Task.
   Context {Task : TaskType}.
diff --git a/restructuring/analysis/task_schedule.v b/restructuring/analysis/task_schedule.v
index 55d062013815633fe3182ae5c2e44cdc75649475..ec3fd834fc346f05d99256d43a1fa959d48dcd15 100644
--- a/restructuring/analysis/task_schedule.v
+++ b/restructuring/analysis/task_schedule.v
@@ -1,6 +1,5 @@
-Require Import rt.restructuring.model.task.
-Require Export rt.restructuring.behavior.all.
-Require Import rt.restructuring.analysis.basic_facts.ideal_schedule.
+Require Export rt.restructuring.model.task.
+Require Export rt.restructuring.analysis.basic_facts.ideal_schedule.
 
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
 
diff --git a/restructuring/model/job_deadline.v b/restructuring/model/job_deadline.v
index 8d112e9ac01d5e67ba7bfc9c2c59ae46618ad81e..a13de3dbf1619c495d2326ec050532491a74da6a 100644
--- a/restructuring/model/job_deadline.v
+++ b/restructuring/model/job_deadline.v
@@ -1,5 +1,5 @@
-Require Import rt.restructuring.model.job.
-Require Import rt.restructuring.model.task.
+Require Export rt.restructuring.model.job.
+Require Export rt.restructuring.model.task.
 
 (** Given task deadlines and a mapping from jobs to tasks 
    we provide a generic definition of job_deadline. *)