From aaf62d5ea27ebd71c433137c28d7c0a606c1ff33 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sat, 20 Jan 2018 19:32:10 +0100
Subject: [PATCH] Fix some comments.

---
 theories/proofmode/classes.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/theories/proofmode/classes.v b/theories/proofmode/classes.v
index 89ebd7374..80d37f3ed 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.
-- 
GitLab