From 47eb79c05ef8a1e541ad7fc8a5b43e30f8946072 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Bjo=CC=88rn=20Brandenburg?= <bbb@mpi-sws.org>
Date: Sun, 17 Jul 2016 13:35:13 +0200
Subject: [PATCH] Trivial fix: use proper processor type in cpu_idle def
---
model/basic/schedule.v | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/model/basic/schedule.v b/model/basic/schedule.v
index ec938aab7..59a423fb2 100644
--- a/model/basic/schedule.v
+++ b/model/basic/schedule.v
@@ -51,7 +51,7 @@ Module Schedule.
[exists cpu, scheduled_on cpu t].
(* A processor cpu is idle at time t if it doesn't contain any jobs. *)
- Definition is_idle (cpu: 'I_(num_cpus)) (t: time) :=
+ Definition is_idle (cpu: processor num_cpus) (t: time) :=
sched cpu t = None.
(* The instantaneous service of job j at time t is the number of cpus
--
GitLab