Commit 0ff98aca authored by sophie quinton's avatar sophie quinton

replace . with ; in proof

parent 6f47832c
......@@ -161,9 +161,9 @@ Module UniprocessorSchedule.
completed_by job_cost sched j t ->
completed_by job_cost sched j t'.
Proof.
unfold completed_by. move => t t' LE /eqP COMPt.
rewrite eqn_leq. apply/andP; split; first by apply H_completed_jobs.
rewrite- COMPt. by apply extend_sum.
unfold completed_by; move => t t' LE /eqP COMPt.
rewrite eqn_leq; apply/andP; split; first by apply H_completed_jobs.
rewrite- COMPt; by apply extend_sum.
Qed.
(* We also prove that a completed job cannot be scheduled. *)
......
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