From b69796e18daa3ede0a2466c6401a31893de02f1f Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Bj=C3=B6rn=20Brandenburg?= <bbb@mpi-sws.org>
Date: Wed, 20 Nov 2019 03:18:27 +0100
Subject: [PATCH] remove unneeded Require statements in basic_facts, core
files, and EDF
---
restructuring/analysis/basic_facts/arrivals.v | 2 +-
restructuring/analysis/basic_facts/completion.v | 2 +-
restructuring/analysis/edf/optimality.v | 4 +---
restructuring/analysis/schedulability.v | 3 ---
restructuring/analysis/task_schedule.v | 5 ++---
restructuring/model/job_deadline.v | 4 ++--
6 files changed, 7 insertions(+), 13 deletions(-)
diff --git a/restructuring/analysis/basic_facts/arrivals.v b/restructuring/analysis/basic_facts/arrivals.v
index 3dabfe00d..a9eb167ab 100644
--- a/restructuring/analysis/basic_facts/arrivals.v
+++ b/restructuring/analysis/basic_facts/arrivals.v
@@ -1,5 +1,5 @@
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.
diff --git a/restructuring/analysis/basic_facts/completion.v b/restructuring/analysis/basic_facts/completion.v
index 53ae48195..d57646ad1 100644
--- a/restructuring/analysis/basic_facts/completion.v
+++ b/restructuring/analysis/basic_facts/completion.v
@@ -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. *)
diff --git a/restructuring/analysis/edf/optimality.v b/restructuring/analysis/edf/optimality.v
index 18942ad7b..121c124f0 100644
--- a/restructuring/analysis/edf/optimality.v
+++ b/restructuring/analysis/edf/optimality.v
@@ -1,6 +1,4 @@
-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
diff --git a/restructuring/analysis/schedulability.v b/restructuring/analysis/schedulability.v
index 2104ea905..ca0048037 100644
--- a/restructuring/analysis/schedulability.v
+++ b/restructuring/analysis/schedulability.v
@@ -1,8 +1,5 @@
-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}.
diff --git a/restructuring/analysis/task_schedule.v b/restructuring/analysis/task_schedule.v
index 55d062013..ec3fd834f 100644
--- a/restructuring/analysis/task_schedule.v
+++ b/restructuring/analysis/task_schedule.v
@@ -1,6 +1,5 @@
-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.
diff --git a/restructuring/model/job_deadline.v b/restructuring/model/job_deadline.v
index 8d112e9ac..a13de3dbf 100644
--- a/restructuring/model/job_deadline.v
+++ b/restructuring/model/job_deadline.v
@@ -1,5 +1,5 @@
-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. *)
--
GitLab