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

remove unneeded Require statements in analysis/transform

parent b69796e1
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. *)
......
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
......
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. *)
......
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
......
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. *)
......
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