diff --git a/restructuring/analysis/edf/optimality.v b/restructuring/analysis/edf/optimality.v
index bed07c60cef893dd5b2236031899c7159daac751..5f3c8e8a34a2ea485ecfbb8fc96f87352b493f29 100644
--- a/restructuring/analysis/edf/optimality.v
+++ b/restructuring/analysis/edf/optimality.v
@@ -6,6 +6,12 @@ From rt.restructuring.analysis Require Import schedulability transform.facts.edf
     (assuming an ideal uniprocessor), then there is also an EDF
     schedule in which all deadlines are met. *)
 
+(** The following results assume ideal uniprocessor schedules... *)
+From rt.restructuring.model.processor Require ideal.
+(** ... and the basic (i.e., Liu & Layland) readiness model under which any
+    pending job is ready. *)
+From rt.restructuring.model.readiness Require basic.
+
 Section Optimality.
   (** For any given type of jobs... *)
   Context {Job : JobType} `{JobCost Job} `{JobDeadline Job} `{JobArrival Job}.
@@ -40,8 +46,10 @@ Section Optimality.
 
 End Optimality.
 
-(** We further state a weaker notion of the above optimality claim
-    that avoids a dependency on a given arrival sequence. *)
+(** We further state a weaker notion of the above optimality claim that avoids
+    a dependency on a given arrival sequence. Specifically, it establishes
+    that, given a reference schedule without deadline misses, there exists an
+    EDF schedule of the same jobs in which no deadlines are missed. *)
 Section WeakOptimality.
 
   (** For any given type of jobs,... *)
diff --git a/restructuring/analysis/transform/edf_trans.v b/restructuring/analysis/transform/edf_trans.v
index 78853374502806ddae68bc933affc9afdf817e17..595bc8078d9dea10bbd4a99bb984db66284042aa 100644
--- a/restructuring/analysis/transform/edf_trans.v
+++ b/restructuring/analysis/transform/edf_trans.v
@@ -45,7 +45,7 @@ Section EDFTransformation.
      t1. *)
   Definition make_edf_at (sched: SchedType) (t1: instant): SchedType :=
     match sched t1 with
-    | None => sched (** leave idle instants alone *)
+    | None => sched (* leave idle instants alone *)
     | Some j =>
       let
         t2 := find_swap_candidate sched t1 j
diff --git a/restructuring/analysis/transform/facts/edf_opt.v b/restructuring/analysis/transform/facts/edf_opt.v
index 528467d907e59c947e34a741094b1b4029c493a2..0ced86adf1c56a9c8049511e958153ef5cbeb223 100644
--- a/restructuring/analysis/transform/facts/edf_opt.v
+++ b/restructuring/analysis/transform/facts/edf_opt.v
@@ -12,9 +12,9 @@ From rt.util Require Import tactics nat.
     schedule. *)
 
 (** Throughout this file, we assume ideal uniprocessor schedules. *)
-From rt.restructuring.model.processor Require Export ideal.
+From rt.restructuring.model.processor Require Import ideal.
 (** Throughout this file, we assume the basic (i.e., Liu & Layland) readiness model. *)
-From rt.restructuring.model.readiness Require Export basic.
+From rt.restructuring.model.readiness Require Import basic.
 
 (** We start by analyzing the helper function [find_swap_candidate],
     which is a problem-specific wrapper around [search_arg]. *)