From 1b7dd3754328dada0674237b148553adfbabb7ff Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Bj=C3=B6rn=20Brandenburg?= <bbb@mpi-sws.org>
Date: Mon, 25 Nov 2019 15:30:40 +0100
Subject: [PATCH] remove unnecessary Require statements in
 model.task.preemption

---
 restructuring/model/task/preemption/floating_nonpreemptive.v | 2 --
 restructuring/model/task/preemption/fully_nonpreemptive.v    | 5 -----
 restructuring/model/task/preemption/fully_preemptive.v       | 2 --
 restructuring/model/task/preemption/limited_preemptive.v     | 1 -
 4 files changed, 10 deletions(-)

diff --git a/restructuring/model/task/preemption/floating_nonpreemptive.v b/restructuring/model/task/preemption/floating_nonpreemptive.v
index 3c801eabc..26b57305b 100644
--- a/restructuring/model/task/preemption/floating_nonpreemptive.v
+++ b/restructuring/model/task/preemption/floating_nonpreemptive.v
@@ -1,8 +1,6 @@
 Require Import rt.restructuring.model.preemption.limited_preemptive.
 Require Export rt.restructuring.model.task.preemption.parameters.
 
-From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.
-
 (** * Platform for Models with Floating Non-Preemptive Regions *)
 (** In this section, we introduce a set of requirements for function
     [task_max_nonpr_segment], so it is coherent with model with
diff --git a/restructuring/model/task/preemption/fully_nonpreemptive.v b/restructuring/model/task/preemption/fully_nonpreemptive.v
index 297fca8b1..becff2100 100644
--- a/restructuring/model/task/preemption/fully_nonpreemptive.v
+++ b/restructuring/model/task/preemption/fully_nonpreemptive.v
@@ -1,7 +1,5 @@
 Require Export rt.restructuring.model.task.preemption.parameters.
 
-From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.
-
 (** * Platform for Fully Non-Preemptive Model *)
 (** In this section, we instantiate function
    [task_max_nonpreemptive_segment] for the fully non-preemptive
@@ -22,9 +20,6 @@ Section FullyNonPreemptiveModel.
                                                      
 End FullyNonPreemptiveModel.
 
-
-From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.
-
 (** * Task's Run to Completion Threshold *)
 (** In this section, we instantiate function [task run to completion
     threshold] for the fully non-preemptive model. *)
diff --git a/restructuring/model/task/preemption/fully_preemptive.v b/restructuring/model/task/preemption/fully_preemptive.v
index 654a20681..8f658cb8a 100644
--- a/restructuring/model/task/preemption/fully_preemptive.v
+++ b/restructuring/model/task/preemption/fully_preemptive.v
@@ -17,8 +17,6 @@ Section FullyPreemptiveModel.
   
 End FullyPreemptiveModel.
 
-Require Export rt.restructuring.model.task.preemption.parameters.
-
 (** * Task's Run to Completion Threshold *)
 (** In this section, we instantiate function [task run to completion
    threshold] for the fully preemptive model. *)
diff --git a/restructuring/model/task/preemption/limited_preemptive.v b/restructuring/model/task/preemption/limited_preemptive.v
index 1dc1094fc..3458aa5bd 100644
--- a/restructuring/model/task/preemption/limited_preemptive.v
+++ b/restructuring/model/task/preemption/limited_preemptive.v
@@ -1,6 +1,5 @@
 Require Export rt.restructuring.model.task.preemption.parameters.
 Require Import rt.restructuring.model.preemption.limited_preemptive.
-From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.
 
 (** * Platform for Models with Limited Preemptions *)
 (** In this section, we introduce a set of requirements for function
-- 
GitLab