diff --git a/behavior/arrival_sequence.v b/behavior/arrival_sequence.v
index 4e9fde5ada178e8ea2b4dc8fbcc7c5ef17dc80b0..c9634a4736219bc279994e3a0460e6714a3f6d9e 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 f503d7ef0451544363843bbd92f1b412651e030f..f95a52a352554ecff853697274fed9edb87a5b71 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 321285c4978e9c08903bd989112e0c542d3f0fe1..6649b18f88317e081f744a03593a2b2715c1abe9 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