From 462b056f6e9e619908f148326fa14b28d6832d24 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 29 Jun 2020 13:51:14 +0200
Subject: [PATCH] Fix typos in docs of `iNext`.

---
 docs/proof_mode.md | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/docs/proof_mode.md b/docs/proof_mode.md
index 5aa8b3e84..dca9f23df 100644
--- a/docs/proof_mode.md
+++ b/docs/proof_mode.md
@@ -134,8 +134,8 @@ Modalities
   and subjectively. The optional argument `mod` can be used to specify what
   modality to introduce in case of ambiguity, e.g. `âŽ¡|==> PâŽ¤`.
 - `iAlways` : a deprecated alias of `iModIntro`.
-- `iNext n` : an alias of `iModIntro (â–·^n P)`.
-- `iNext` : an alias of `iModIntro (â–·^1 P)`.
+- `iNext n` : an alias of `iModIntro (â–·^n _)`.
+- `iNext` : an alias of `iModIntro (â–·^_ _)`.
 - `iMod pm_trm as (x1 ... xn) "ipat"` : eliminate a modality `pm_trm` that is
   an instance of the `ElimModal` type class. Instances include: later, except 0,
   basic update and fancy update.
-- 
GitLab