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

remove unneeded Require statements in model/schedule

parent 9a8c6b13
Require Import rt.util.all.
Require Import rt.restructuring.behavior.all.
Require Export rt.restructuring.behavior.all.
Require Import rt.restructuring.model.job.
Require Import rt.restructuring.model.task.
Require Import rt.restructuring.model.processor.ideal.
Require Import rt.restructuring.model.preemption.job.parameters.
Require Export rt.restructuring.model.preemption.job.parameters.
Require Import rt.restructuring.model.preemption.task.parameters.
Require Import rt.restructuring.model.preemption.valid_model.
From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.
......
Require Import rt.restructuring.behavior.all.
Require Import rt.restructuring.model.job.
Require Export rt.restructuring.model.job.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
(** In this section we introduce the notion of a non-preemptive schedule. *)
......
Require Import rt.restructuring.model.job.
Require Import rt.restructuring.model.task.
Require Import rt.restructuring.model.job_deadline.
Require Export rt.restructuring.model.job_deadline.
Require Import rt.restructuring.model.schedule.priority_based.priorities.
From mathcomp Require Export seq.
......
Require Import rt.restructuring.behavior.all.
Require Import rt.restructuring.model.schedule.priority_based.priorities.
Require Import rt.restructuring.model.processor.ideal.
Require Import rt.restructuring.model.preemption.preemption_time.
Require Import rt.restructuring.model.preemption.job.parameters.
Require Export rt.restructuring.model.schedule.priority_based.priorities.
Require Export rt.restructuring.model.preemption.preemption_time.
(** We now define what it means for a schedule to respect a priority
in the presence of jobs with non-preemptive segments. *)
......
Require Export rt.restructuring.behavior.all.
Require Export rt.restructuring.model.schedule.priority_based.priorities.
(** We now define what it means for a schedule to respect a priority *)
......
Require Export rt.restructuring.behavior.all.
Require Export rt.restructuring.model.task.
Section PropertyOfSequentiality.
......
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