From eff367aaea9e4fb76b207d49c21ac7adc9b82de9 Mon Sep 17 00:00:00 2001
From: Sergei Bozhko <sbozhko@mpi-sws.org>
Date: Tue, 28 Sep 2021 10:26:53 +0200
Subject: [PATCH] move [Context] declaration out of the global context
---
model/task/arrival/arrival_curve_to_rbf.v | 12 ++++++------
1 file changed, 6 insertions(+), 6 deletions(-)
diff --git a/model/task/arrival/arrival_curve_to_rbf.v b/model/task/arrival/arrival_curve_to_rbf.v
index c76073dfc..27d3c62d9 100644
--- a/model/task/arrival/arrival_curve_to_rbf.v
+++ b/model/task/arrival/arrival_curve_to_rbf.v
@@ -4,18 +4,18 @@ Require Export prosa.model.task.arrival.curves.
(** * Converting an Arrival Curve + Worst-Case/Best-Case to a Request-Bound Function (RBF) *)
-(** Consider any type of tasks with a given cost ... *)
-Context {Task : TaskType} `{TaskCost Task} `{TaskMinCost Task}.
-
-(** ... and any type of jobs associated with these tasks. *)
-Context {Job : JobType} `{JobTask Job Task} `{JobCost Job}.
-
(** In the following, we show a way to convert a given arrival curve,
paired with a worst-case/best-case execution time, to a request-bound function.
Definitions and proofs will handle both lower-bounding and upper-bounding arrival
curves. *)
Section ArrivalCurveToRBF.
+ (** Consider any type of tasks with a given cost ... *)
+ Context {Task : TaskType} `{TaskCost Task} `{TaskMinCost Task}.
+
+ (** ... and any type of jobs associated with these tasks. *)
+ Context {Job : JobType} `{JobTask Job Task} `{JobCost Job}.
+
(** Let [MaxArr] and [MinArr] represent two arrivals curves. [MaxArr] upper-bounds
the possible number or arrivals for a given task, whereas [MinArr] lower-bounds it. *)
Context `{MaxArr : MaxArrivals Task} `{MinArr : MinArrivals Task}.
--
GitLab