Make the floating preemptive model hypothesis more explicit

analysis/facts/preemption/rtc_threshold/floating.v

 Require Export prosa.analysis.facts.preemption.task.floating.
 Require Export prosa.analysis.facts.preemption.rtc_threshold.job_preemptable.
-
-(** Furthermore, we assume the task model with floating non-preemptive regions. *)
-Require Import prosa.model.preemption.limited_preemptive.
 Require Import prosa.model.task.preemption.floating_nonpreemptive.
 
 (** * Task's Run to Completion Threshold *)
@@ -10,6 +7,9 @@ Require Import prosa.model.task.preemption.floating_nonpreemptive.
     threshold] for the model with floating non-preemptive regions. *)
 Section TaskRTCThresholdFloatingNonPreemptiveRegions.
 
+  (** Furthermore, we assume the task model with floating non-preemptive regions. *)
+  #[local] Existing Instance floating_preemptive.
+
   (** Consider any type of tasks ... *)
   Context {Task : TaskType}.
   Context `{TaskCost Task}.

model/task/preemption/floating_nonpreemptive.v

@@ -59,9 +59,7 @@ Section TaskRTCThresholdFloatingNonPreemptiveRegions.
       information about the placement of preemption points in all jobs, i.e.,
       it is impossible to predict when exactly a job will be preemptable. Thus,
       the only safe run-to-completion threshold is [task cost]. *)
-  Global Program Instance fully_preemptive : TaskRunToCompletionThreshold Task :=
-    {
-      task_rtct (tsk : Task) := task_cost tsk
-    }.
+  Definition floating_preemptive : TaskRunToCompletionThreshold Task :=
+    fun tsk : Task => task_cost tsk.
 
 End TaskRTCThresholdFloatingNonPreemptiveRegions.