Commit 4134d178 authored by Felipe Cerqueira's avatar Felipe Cerqueira

Fix typo after removing unused definition

parent 0b7ad51c
......@@ -830,7 +830,6 @@ Module ResponseTimeIterationEDF.
(tsk, R) \in rt_bounds ->
R = rt_recurrence tsk rt_bounds R.
Proof.
unfold least_fixed_point.
intros tsk R rt_bounds SOME IN.
have CONV := edf_claimed_bounds_finds_fixed_point_of_list rt_bounds.
rewrite -iterS in CONV; fold (f (max_steps ts).+1) in CONV.
......
......@@ -885,7 +885,6 @@ Module ResponseTimeIterationEDF.
(tsk, R) \in rt_bounds ->
R = rt_recurrence tsk rt_bounds R.
Proof.
unfold least_fixed_point.
intros tsk R rt_bounds SOME IN.
have CONV := edf_claimed_bounds_finds_fixed_point_of_list rt_bounds.
rewrite -iterS in CONV; fold (f (max_steps ts).+1) in CONV.
......
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