diff --git a/Lang.agda b/Lang.agda
index 3eb2437..a55b379 100644
--- a/Lang.agda
+++ b/Lang.agda
@@ -151,7 +151,7 @@ basict₁ = pushint-t thenᵗ pushint-t thenᵗ pushint-t thenᵗ add-t thenᵗ
 -- basict₂ : ([] ⟨ []  ⟩) ⊢ (loop 1 ∷ pushbool true ∷ break ∷ pushint (+ 1) ∷ end ∷ []) ↦* ([] ⟨ [] ⟩)
 -- basict₂ = loop-t thenᵗ pushbool-t thenᵗ break-t thenᵗ pushint-t thenᵗ end-t thenᵗ doneᵗ
 
--- Fast forwarding to a 'break' in will peel off one continuation (since that
+-- Fast forwarding to a 'break' will peel off one continuation (since that
 -- continuation encodes the post-loop type).
 lemma₁ : ∀ {lst} → st ⟨ lst ∷ F ⟩ ⊢ is ↦* σ → is ⇒ₓ is' → lst ⟨ F ⟩ ⊢ is' ↦* σ
 lemma₁ doneᵗ ()
@@ -194,7 +194,7 @@ data ⟦_⟧ˢ : List ValueType → List Value → Set where
 -- Parameterize by final stack type. The reason to do this is that we want
 -- all continuations to end in the same type, so that control flow doesn't change
 -- what final type the program is evaluated to. This is an unfortunate consequence
--- of having to include copies of the program as part of the type.
+-- of having to include copies of the rest of the program as part of execution.
 module _ (stˡ : List ValueType) where
     data ⟦_⟧ᶠ : List (List ValueType) → Program → Env → Set where
         ⟦⟧ᶠ-empty : ⟦ [] ⟧ᶠ is []