Skip to content
Snippets Groups Projects
Commit bd0e5427 authored by Björn Brandenburg's avatar Björn Brandenburg
Browse files

fix deprecation warning in classic global schedule

This change breaks compatibility with mathcomp < 1.10.
parent 5312542f
No related branches found
No related tags found
1 merge request!104Support mathcomp 1.11.0 and Coq 8.12
......@@ -226,7 +226,7 @@ Module Schedule.
{
move: SCHED => /existsP [cpu SCHED]; des.
rewrite -big_filter (bigD1_seq cpu);
[simpl | | by rewrite filter_index_enum enum_uniq];
[simpl | | by have [e _ [UNIQ _ ] _] := big_enumP];
last by rewrite mem_filter; apply/andP; split.
rewrite -big_filter -filter_predI big_filter.
rewrite -> eq_bigr with (F2 := fun cpu => 0);
......@@ -610,4 +610,4 @@ Module ScheduleOfSporadicTask.
End BasicLemmas.
End ScheduleOfSporadicTask.
\ No newline at end of file
End ScheduleOfSporadicTask.
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment