Polish

implementation/facts/ideal_uni/preemption_aware.v

@@ -86,7 +86,7 @@ Section NPUniprocessorScheduler.
         by apply schedule_up_to_prefix_inclusion. }
       { elim: t IDLE NONE => [IDLE _| t' _ _ ->]; last by rewrite schedule_up_to_empty.
         rewrite /schedule_up_to replace_at_def.
-        rewrite /allocation_at /prev_job_nonpreemptive IDLE H_non_idling //. }
+        by rewrite /allocation_at /prev_job_nonpreemptive IDLE H_non_idling. }
     Qed.
 
     (** From the preceding fact, we conclude that the generated schedule is

implementation/facts/ideal_uni/prio_aware.v

@@ -76,7 +76,7 @@ Section PrioAwareUniprocessorScheduler.
     Corollary schedule_respects_preemption_model :
       schedule_respects_preemption_model arr_seq schedule.
     Proof.
-      by apply np_respects_preemption_model .
+      by apply np_respects_preemption_model.
     Qed.
 
   End PreemptionCompliance.