diff --git a/model/processor/varspeed.v b/model/processor/varspeed.v
index d03f3629343e5a727d7fdc43fe315c39bd5a28cd..73a19bbd7d5f935a3f90115266c9bfe601771dbe 100644
--- a/model/processor/varspeed.v
+++ b/model/processor/varspeed.v
@@ -45,12 +45,12 @@ Section State.
 
   (** Finally, we connect the above definitions to the generic Prosa interface
       for processor states. *)
-  Global Program Instance pstate_instance : ProcessorState Job :=
-    {
+  Program Definition pstate_instance : ProcessorState Job :=
+    {|
       State := processor_state;
       scheduled_on := varspeed_scheduled_on;
       service_on   := varspeed_service_on
-    }.
+    |}.
   Next Obligation.
     move: r H.
     case: s=>//= j' v _.