From 1d1fe891841c0049bcc63367f91ce24e86f47ef1 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Bj=C3=B6rn=20Brandenburg?= <bbb@mpi-sws.org> Date: Fri, 28 Feb 2025 08:52:20 +0100 Subject: [PATCH] fix comment --- analysis/definitions/finish_time.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/analysis/definitions/finish_time.v b/analysis/definitions/finish_time.v index 3026d5258..18d92487d 100644 --- a/analysis/definitions/finish_time.v +++ b/analysis/definitions/finish_time.v @@ -45,7 +45,7 @@ Section JobFinishTime. Definition finish_time : instant := ex_minn job_finishes. (** In the following, we demonstrate the reuse of [ex_minn] properties by - establishing two natural properties of a job's finish time. *) + establishing three natural properties of a job's finish time. *) (** First, a job is indeed complete at its finish time. *) Corollary finished_at_finish_time : completed_by sched j finish_time. -- GitLab