diff --git a/theories/proofmode/classes.v b/theories/proofmode/classes.v
index 89ebd7374f2742282fd7ca030d8ac8df879520de..80d37f3ed854827a8180344c7b5506d2f4e26d4d 100644
--- a/theories/proofmode/classes.v
+++ b/theories/proofmode/classes.v
@@ -84,7 +84,7 @@ Hint Mode FromAlways + - ! - : typeclass_instances.
   progress, i.e. its instances should actually strip a later.
 
 The point of using the auxilary class [IntoLaterN'] is to ensure that the
-default instance is not applied deeply in the term, which may cause in too many
+default instance is not applied deeply in the term, which may result in too many
 definitions being unfolded (see issue #55).
 
 For binary connectives we have the following instances:
@@ -97,7 +97,7 @@ IntoLaterN' n P P'       IntoLaterN n Q Q'
 
       IntoLaterN' n Q Q'
 -------------------------------
-IntoLaterN n (P /\ Q) (P /\ Q')
+IntoLaterN' n (P /\ Q) (P /\ Q')
 >>
 *)
 Class IntoLaterN {M} (n : nat) (P Q : uPred M) := into_laterN : P ⊢ ▷^n Q.