Commit b69796e1 authored by Björn Brandenburg's avatar Björn Brandenburg

remove unneeded Require statements in basic_facts, core files, and EDF

parent 17a1bb81
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.
......
......@@ -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. *)
......
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
......
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}.
......
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.
......
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. *)
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment