From 12b573c3239f630f6d12e357ab0b11049aee9374 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Bj=C3=B6rn=20Brandenburg?= <bbb@mpi-sws.org>
Date: Fri, 22 Nov 2019 20:48:50 +0100
Subject: [PATCH] remove task dependency in job limited-preemptive preemption
model
Job-level definitions should not depend on task-related modules.
---
restructuring/model/preemption/limited_preemptive.v | 1 -
restructuring/model/task/preemption/floating_nonpreemptive.v | 1 +
restructuring/model/task/preemption/limited_preemptive.v | 1 +
3 files changed, 2 insertions(+), 1 deletion(-)
diff --git a/restructuring/model/preemption/limited_preemptive.v b/restructuring/model/preemption/limited_preemptive.v
index d4345918c..9af1016a5 100644
--- a/restructuring/model/preemption/limited_preemptive.v
+++ b/restructuring/model/preemption/limited_preemptive.v
@@ -1,5 +1,4 @@
Require Export rt.restructuring.model.preemption.parameter.
-Require Export rt.restructuring.model.task.preemption.parameters.
(** Definition of a parameter relating a job
to the sequence of its preemption points. *)
diff --git a/restructuring/model/task/preemption/floating_nonpreemptive.v b/restructuring/model/task/preemption/floating_nonpreemptive.v
index d0e75b0ac..a66d11cc5 100644
--- a/restructuring/model/task/preemption/floating_nonpreemptive.v
+++ b/restructuring/model/task/preemption/floating_nonpreemptive.v
@@ -1,4 +1,5 @@
Require Export 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.
diff --git a/restructuring/model/task/preemption/limited_preemptive.v b/restructuring/model/task/preemption/limited_preemptive.v
index 343a6db76..aa33cabca 100644
--- a/restructuring/model/task/preemption/limited_preemptive.v
+++ b/restructuring/model/task/preemption/limited_preemptive.v
@@ -1,4 +1,5 @@
Require Export 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.
--
GitLab