From 049df491f14b39bd47faeacb80a5825cf6298fa5 Mon Sep 17 00:00:00 2001
From: Pierre Roux <pierre.roux@onera.fr>
Date: Mon, 20 Feb 2023 16:36:23 +0100
Subject: [PATCH] [tutorial] Avoid introducing the `{...} syntax
---
behavior/arrival_sequence.v | 16 ++++++++--------
behavior/service.v | 6 +++---
doc/tutorial.v | 12 ++++++------
3 files changed, 17 insertions(+), 17 deletions(-)
diff --git a/behavior/arrival_sequence.v b/behavior/arrival_sequence.v
index 4e9fde5ad..c9634a473 100644
--- a/behavior/arrival_sequence.v
+++ b/behavior/arrival_sequence.v
@@ -47,8 +47,8 @@ Section ValidArrivalSequence.
(** Assume that job arrival times are known. *)
Context {Job: JobType}.
- Context `{JobArrival Job}.
-
+ Context {ja : JobArrival Job}.
+
(** Consider any job arrival sequence. *)
Variable arr_seq: arrival_sequence Job.
@@ -75,11 +75,11 @@ End ValidArrivalSequence.
Section ArrivalTimeProperties.
(** Assume that job arrival times are known. *)
- Context {Job: JobType}.
- Context `{JobArrival Job}.
+ Context {Job : JobType}.
+ Context {ja : JobArrival Job}.
(** Let j be any job. *)
- Variable j: Job.
+ Variable j : Job.
(** We say that job j has arrived at time t iff it arrives at some time t_0
with t_0 <= t. *)
@@ -102,11 +102,11 @@ End ArrivalTimeProperties.
Section ArrivalSequencePrefix.
(** Assume that job arrival times are known. *)
- Context {Job: JobType}.
- Context `{JobArrival Job}.
+ Context {Job : JobType}.
+ Context {ja : JobArrival Job}.
(** Consider any job arrival sequence. *)
- Variable arr_seq: arrival_sequence Job.
+ Variable arr_seq : arrival_sequence Job.
(** By concatenation, we construct the list of jobs that arrived in the
interval <<[t1, t2)>>. *)
diff --git a/behavior/service.v b/behavior/service.v
index f503d7ef0..f95a52a35 100644
--- a/behavior/service.v
+++ b/behavior/service.v
@@ -35,9 +35,9 @@ Section Service.
(** In the following, consider jobs that have a cost, a deadline, and an
arbitrary arrival time. *)
- Context `{JobCost Job}.
- Context `{JobDeadline Job}.
- Context `{JobArrival Job}.
+ Context {jc : JobCost Job}.
+ Context {jd : JobDeadline Job}.
+ Context {ja : JobArrival Job}.
(** We say that job [j] has completed by time [t] if it received all required
service in the interval from [0] until (but not including) [t]. *)
diff --git a/doc/tutorial.v b/doc/tutorial.v
index 321285c49..6649b18f8 100644
--- a/doc/tutorial.v
+++ b/doc/tutorial.v
@@ -433,7 +433,7 @@ Section ValidArrivalSequence.
(** Assume that job arrival times are known. *)
Context {Job : JobType}.
- Context `{JobArrival Job}.
+ Context {ja : JobArrival Job}.
(** Consider any job arrival sequence. *)
Variable arr_seq : arrival_sequence Job.
@@ -463,7 +463,7 @@ Section ArrivalTimeProperties.
(** Assume that job arrival times are known. *)
Context {Job : JobType}.
- Context `{JobArrival Job}.
+ Context {ja : JobArrival Job}.
(** Let j be any job. *)
Variable j : Job.
@@ -490,7 +490,7 @@ Section ArrivalSequencePrefix.
(** Assume that job arrival times are known. *)
Context {Job : JobType}.
- Context `{JobArrival Job}.
+ Context {ja : JobArrival Job}.
(** Consider any job arrival sequence. *)
Variable arr_seq : arrival_sequence Job.
@@ -592,9 +592,9 @@ as well as the notion of completion of a job
|*)
(** In the following, consider jobs that have a cost, a deadline,
and an arbitrary arrival time. *)
- Context `{JobCost Job}.
- Context `{JobDeadline Job}.
- Context `{JobArrival Job}.
+ Context {jc : JobCost Job}.
+ Context {jd : JobDeadline Job}.
+ Context {ja : JobArrival Job}.
(** We say that job [j] has completed by time [t] if it received all
required service in the interval from [0] until
--
GitLab