diff --git a/restructuring/model/arrival/arrival_curves.v b/restructuring/model/arrival/arrival_curves.v index f6cd2ac511620c1535661845bd7e48f557c41715..f89c3df92d2a697505a87907282291e6d65cfda0 100644 --- a/restructuring/model/arrival/arrival_curves.v +++ b/restructuring/model/arrival/arrival_curves.v @@ -1,6 +1,5 @@ -Require Import rt.util.all. -Require Export rt.restructuring.behavior.all. -Require Import rt.restructuring.model.aggregate.task_arrivals. +Require Export rt.util.rel. +Require Export rt.restructuring.model.aggregate.task_arrivals. (** In this section, we define the notion of arrival curves, which can be used to reason about the frequency of job arrivals. *) diff --git a/restructuring/model/arrival/sporadic.v b/restructuring/model/arrival/sporadic.v index 6dc889ba1a5ccd3b06d2c90620263cc0402afcf6..3806e931c63aecc1a14336cae96534ddef1a286a 100644 --- a/restructuring/model/arrival/sporadic.v +++ b/restructuring/model/arrival/sporadic.v @@ -1,4 +1,3 @@ -Require Export rt.restructuring.behavior.all. Require Export rt.restructuring.model.task. Section TaskMinInterArrivalTime.