From 54e7671c502cb7697026109b38395d0efea602a3 Mon Sep 17 00:00:00 2001
From: Dan Frumin <dan@covariant.me>
Date: Thu, 16 Mar 2017 10:57:06 +0100
Subject: [PATCH] IntoModal --> FromModal in the docs

---
 ProofMode.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/ProofMode.md b/ProofMode.md
index 29807cb9e..2071dd351 100644
--- a/ProofMode.md
+++ b/ProofMode.md
@@ -113,7 +113,7 @@ Modalities
 ----------
 
 - `iModIntro` : introduction of a modality that is an instance of the
-  `IntoModal` type class. Instances include: later, except 0, basic update and
+  `FromModal` type class. Instances include: later, except 0, basic update and
   fancy update.
 - `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,
-- 
GitLab