From f1ff74c25c0f1edb69de7bd270011ef96b54cf90 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:22:35 +0100
Subject: [PATCH] remove unneeded Require statements in analysis/transform
---
restructuring/analysis/transform/edf_trans.v | 1 -
restructuring/analysis/transform/facts/edf_opt.v | 4 ----
restructuring/analysis/transform/facts/replace_at.v | 2 --
restructuring/analysis/transform/prefix.v | 3 +--
restructuring/analysis/transform/swap.v | 3 +--
5 files changed, 2 insertions(+), 11 deletions(-)
diff --git a/restructuring/analysis/transform/edf_trans.v b/restructuring/analysis/transform/edf_trans.v
index 210d7675c..65ed0841b 100644
--- a/restructuring/analysis/transform/edf_trans.v
+++ b/restructuring/analysis/transform/edf_trans.v
@@ -1,6 +1,5 @@
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. *)
diff --git a/restructuring/analysis/transform/facts/edf_opt.v b/restructuring/analysis/transform/facts/edf_opt.v
index db2e81b48..1be7c88f9 100644
--- a/restructuring/analysis/transform/facts/edf_opt.v
+++ b/restructuring/analysis/transform/facts/edf_opt.v
@@ -1,14 +1,10 @@
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
diff --git a/restructuring/analysis/transform/facts/replace_at.v b/restructuring/analysis/transform/facts/replace_at.v
index 9b0f7ed3f..5e22b2dfe 100644
--- a/restructuring/analysis/transform/facts/replace_at.v
+++ b/restructuring/analysis/transform/facts/replace_at.v
@@ -1,6 +1,4 @@
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. *)
diff --git a/restructuring/analysis/transform/prefix.v b/restructuring/analysis/transform/prefix.v
index d7fd08aa1..288b202d8 100644
--- a/restructuring/analysis/transform/prefix.v
+++ b/restructuring/analysis/transform/prefix.v
@@ -1,6 +1,5 @@
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
diff --git a/restructuring/analysis/transform/swap.v b/restructuring/analysis/transform/swap.v
index 0ffa02502..96dc092d2 100644
--- a/restructuring/analysis/transform/swap.v
+++ b/restructuring/analysis/transform/swap.v
@@ -1,5 +1,4 @@
-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. *)
--
GitLab