Commit aae959e6 authored by Pierre Roux's avatar Pierre Roux

Compile with mathcomp 1.10

parent ee05f255
......@@ -198,7 +198,7 @@ Module PolicyTDMA.
have SO2:O2 + task_time_slot tsk2 <= cycle by apply (Offset_add_slot_leq_cycle tsk2).
repeat rewrite mod_elim;auto.
case (O1 <= t%%cycle)eqn:O1T;case (O2 <= t %%cycle)eqn:O2T;intros G1 G2;try ssromega.
apply ltn_subLR in G1;apply ltn_subLR in G2. case (tsk1==tsk2) eqn:NEQ;move/eqP in NEQ;auto.
apply util.nat.ltn_subLR in G1;apply util.nat.ltn_subLR in G2. case (tsk1==tsk2) eqn:NEQ;move/eqP in NEQ;auto.
destruct (slot_order_total tsk1 tsk2) as [order |order];auto;apply relation_offset in order;
fold O1 O2 in order;try ssromega;auto. by move/eqP in NEQ. apply /eqP;auto.
Qed.
......
......@@ -223,7 +223,7 @@ Module RTAforEDFwithBoundedNonpreemptiveSegmentsWithArrivalCurves.
rewrite addn1 addnS in H.
rewrite -subn_gt0 in H0.
apply ltn_trans with (a - c + b); last by done.
apply ltn_subLR.
apply util.nat.ltn_subLR.
have EQ: b - b = 0. apply/eqP. rewrite subn_eq0. by done.
by rewrite EQ.
}
......
......@@ -46,3 +46,5 @@ extremum
supremum
runtime
bursty
TODO
mathcomp
......@@ -54,6 +54,7 @@ Section NatLemmas.
induction b;induction c;intros;try ssromega.
Qed.
(* TODO: remove when mathcomp minimum required version becomes 1.10.0 *)
Lemma ltn_subLR:
forall a b c,
a - c < b ->
......
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