Commit c95b4984 authored by Björn Brandenburg's avatar Björn Brandenburg

fix minor warning

parent 877d6625
Pipeline #33776 passed with stages
in 17 minutes and 47 seconds
......@@ -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.
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment