Remove sequential readiness Global Instance

model/readiness/sequential.v

@@ -27,12 +27,11 @@ Section SequentialTasksReadiness.
   (* A job [j] is ready at a time instant [t] iff all jobs from task
      [job_task j] that arrived earlier than job [j] are already
      completed by time [t]. *)
-  Global Program Instance sequential_ready_instance : JobReady Job PState :=
-    {
-    job_ready sched j t :=
-      pending sched j t &&
-      prior_jobs_complete arr_seq sched j t
-    }.
+  #[local,program] Instance sequential_ready_instance : JobReady Job PState :=
+  {
+    job_ready sched j t := pending sched j t &&
+                             prior_jobs_complete arr_seq sched j t
+  }.
   Next Obligation. by move: H2 => /andP[]. Qed.
 
 End SequentialTasksReadiness.