diff --git a/model/task/preemption/fully_preemptive.v b/model/task/preemption/fully_preemptive.v index f8b4836e6ee8448c96a81ff51596e66621d1945f..fab0a930db9f28789454e132d5d9e9ca62466dbf 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 ε