diff --git a/analysis/definitions/finish_time.v b/analysis/definitions/finish_time.v
index 630a75267fcf88ee2fd57ca5dd4d57546dc9c133..3026d525807ca14aa4c5324158e1a2c6e57921f9 100644
--- a/analysis/definitions/finish_time.v
+++ b/analysis/definitions/finish_time.v
@@ -29,7 +29,7 @@ Section JobFinishTime.
 
   (** In the following, we proceed under the assumption that [j] finishes
       eventually (i.e., no later than [R] time units after its arrival, for any
-      finite [R]), ... *)
+      finite [R]). *)
   Variable R : nat.
   Hypothesis H_response_time_bounded : job_response_time_bound sched j R.