From 224fa2582f3a8754b0b4bbd2d3fd9bda0f739791 Mon Sep 17 00:00:00 2001
From: Marco Maida <>
Date: Wed, 5 Aug 2020 14:58:38 +0200
Subject: [PATCH] Fixed error in classic
---
classic/model/schedule/uni/susp/build_suspension_table.v | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/classic/model/schedule/uni/susp/build_suspension_table.v b/classic/model/schedule/uni/susp/build_suspension_table.v
index 338345b96..697a6edfe 100644
--- a/classic/model/schedule/uni/susp/build_suspension_table.v
+++ b/classic/model/schedule/uni/susp/build_suspension_table.v
@@ -226,7 +226,7 @@ Module SuspensionTableConstruction.
by rewrite EQ /= in ALL; apply/eqP; rewrite eqb0.
}
move => /existsP [t0 /andP [/eqP EQ SUSP0]].
- have MAX := @arg_maxP _ t0 (fun x=>(S j x == S j (ex j t)) && susp_at j x) id.
+ have MAX := @arg_maxnP _ t0 (fun x=>(S j x == S j (ex j t)) && susp_at j x) id.
feed MAX; simpl in MAX; first by rewrite EQ eq_refl SUSP0.
move: MAX => [m /andP [/eqP EQserv SUSPm] ALL]; clear EQ SUSP0 t0.
case (ltnP t m) => [LTm | GEm].
--
GitLab