From c95b4984df2050ac946dd3cfd778848f1105d70a Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Bj=C3=B6rn=20Brandenburg?= Date: Wed, 9 Sep 2020 11:01:10 +0200 Subject: [PATCH] fix minor warning --- analysis/facts/periodic/arrival_times.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/analysis/facts/periodic/arrival_times.v b/analysis/facts/periodic/arrival_times.v index 164cf83..15a7501 100644 --- a/analysis/facts/periodic/arrival_times.v +++ b/analysis/facts/periodic/arrival_times.v @@ -84,7 +84,7 @@ Section PeriodicArrivalTimes. apply first_job_arrival with (tsk0 := tsk) in EQ => //. now rewrite EQ in ARR; ssrlia. } - move : H_task_respects_periodic_model => [j' [ARR' [IND' [TSK' [ARRIVAL']]]]]. + move : H_task_respects_periodic_model => [j' [ARR' [IND' [TSK' ARRIVAL']]]]. specialize (IHn j'); feed_n 3 IHn => //; first by rewrite ARR in ARRIVAL'; ssrlia. rewrite IHn in IND'. destruct (PeanoNat.Nat.zero_or_succ (job_index arr_seq j)) as [Z | [m SUCC]]; last by ssrlia. -- GitLab