From cd10f5a69ea2f270f01ad216cf696f36a4a18565 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 17 Feb 2017 20:37:13 +0100
Subject: [PATCH] Fix typos.

---
 ProofMode.md | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/ProofMode.md b/ProofMode.md
index 17ccf47b8..3bb6cc044 100644
--- a/ProofMode.md
+++ b/ProofMode.md
@@ -124,8 +124,8 @@ The later modality
 
 - `iNext n` : introduce `n` laters by stripping that number of laters from all
   hypotheses. If the argument `n` is not given, it strips one later if the
-  leftmost conjuct is of the shape `â–· P`, or `n` laters if the leftmost conjuct
-  is of the shape `â–·^n P`.
+  leftmost conjunct is of the shape `â–· P`, or `n` laters if the leftmost
+  conjunct is of the shape `â–·^n P`.
 - `iLöb as "IH" forall (x1 ... xn) "selpat"` : perform Löb induction by
   generating a hypothesis `IH : â–· goal`. The tactic generalizes over the Coq
   level variables `x1 ... xn`, the hypotheses given by the selection pattern
-- 
GitLab