diff --git a/restructuring/behavior/ready.v b/restructuring/behavior/ready.v
index 50b1fd88245d7d742b1febe1c615e45d7f5ad204..90361a6626fe85a9740682d2b6b30d7a7510fc87 100644
--- a/restructuring/behavior/ready.v
+++ b/restructuring/behavior/ready.v
@@ -25,7 +25,7 @@ Class JobReady (Job : JobType) (PState : Type)
 (** Based on the general notion of readiness, we define what it means to be
    backlogged, i.e., ready to run but not executing. *)
 Section Backlogged.
-  (** Conside any kinds of jobs and any kind of processor state. *)
+  (** Consider any kinds of jobs and any kind of processor state. *)
   Context {Job : JobType} {PState : Type}.
   Context `{ProcessorState Job PState}.
 
@@ -79,7 +79,7 @@ Section ValidSchedule.
     jobs_must_be_ready_to_execute.
 
   (** Note that we do not explicitly require that a valid schedule satisfies
-     jobs_must_arrive_to_execute or completed_jobs_dont_execute because these
+     [jobs_must_arrive_to_execute] or [completed_jobs_dont_execute] because these
      properties are implied by jobs_must_be_ready_to_execute. *)
 
 End ValidSchedule.
diff --git a/restructuring/behavior/schedule.v b/restructuring/behavior/schedule.v
index 6801eaf43d85407900b7622122ecda864262d1c3..cba3f33ebff15997f2cbd2a1e61f39b1f104ca13 100644
--- a/restructuring/behavior/schedule.v
+++ b/restructuring/behavior/schedule.v
@@ -6,7 +6,7 @@ Require Export rt.restructuring.behavior.arrival_sequence.
 (** Rather than choosing a specific schedule representation up front, we define
     the notion of a generic processor state, which allows us to state general
     definitions of core concepts (such as "how much service has a job
-    received") that work across many possble scenarios (e.g., ideal
+    received") that work across many possible scenarios (e.g., ideal
     uniprocessor schedules, schedules with overheads, variable-speed
     processors, multiprocessors, etc.).
 
diff --git a/restructuring/behavior/time.v b/restructuring/behavior/time.v
index 54dd8b230189a797b8c7f3b3c2307595a19aeebd..58fb14fa2185cf4d699190687c1aff4c1dac5eee 100644
--- a/restructuring/behavior/time.v
+++ b/restructuring/behavior/time.v
@@ -1,8 +1,8 @@
 (** * Model of Time *)
 
 (** Prosa is based on a discrete model of time. Thus, time is simply defined by
-    the natural numbers. To aid readability, we distinguish between time values
-    that represent durations and time values that represent specific
-    instants. *)
+    the natural numbers. To aid readability, we distinguish between values of time
+    that represent a duration and values of time that represent a specific
+    instant. *)
 Definition duration := nat.
 Definition instant  := nat.