From 9aca7702ee2d9b90e07aa89a20bd795f780b95c0 Mon Sep 17 00:00:00 2001 From: kimaya <f20171026@goa.bits-pilani.ac.in> Date: Thu, 7 Oct 2021 15:27:18 +0200 Subject: [PATCH] fix misleading type `Task` should obviously be of type `TaskType`. --- model/task/preemption/fully_preemptive.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/model/task/preemption/fully_preemptive.v b/model/task/preemption/fully_preemptive.v index f8b4836e6..fab0a930d 100644 --- a/model/task/preemption/fully_preemptive.v +++ b/model/task/preemption/fully_preemptive.v @@ -8,7 +8,7 @@ Require Export prosa.model.task.preemption.parameters. Section FullyPreemptiveModel. (** Consider any type of jobs. *) - Context {Task : JobType}. + Context {Task : TaskType}. (** In the fully preemptive model, any job can be preempted at any time. Thus, the maximal non-preemptive segment has length at most ε -- GitLab