diff --git a/model/processor/multiprocessor.v b/model/processor/multiprocessor.v
index c4cd507ea8263dcf921b08c051ed33969e3e495f..1131457e485d32f435eb7f16496653d20ea02f87 100644
--- a/model/processor/multiprocessor.v
+++ b/model/processor/multiprocessor.v
@@ -58,12 +58,12 @@ Section Schedule.
 
   (** Finally, we connect the above definitions with the generic Prosa
       interface for processor models. *)
-  Global Program Instance multiproc_state : ProcessorState Job :=
-    {
+  #[local] Program Instance multiproc_state : ProcessorState Job :=
+    {|
       State := multiprocessor_state;
       scheduled_on := multiproc_scheduled_on;
       service_on := multiproc_service_on
-    }.
+    |}.
   Next Obligation.
     move: j s r H.
     move=> j mps cpu.