[tutorial] Avoid introducing the `{...} syntax

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)>>. *)

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]. *)

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