From b2426163c4187d4545d4383ab9c47d186d9740a1 Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Tue, 13 Feb 2018 13:44:30 +0100
Subject: [PATCH] Fix doc.

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

diff --git a/theories/proofmode/classes.v b/theories/proofmode/classes.v
index 409d92274..0a2261f32 100644
--- a/theories/proofmode/classes.v
+++ b/theories/proofmode/classes.v
@@ -43,15 +43,15 @@ Proof. by exists φ. Qed.
 Hint Extern 0 (IntoPureT _ _) =>
   notypeclasses refine (into_pureT_hint _ _ _) : typeclass_instances.
 
-(** [FromPure] is used when introducing a pure assertion. It is used by
-    iPure, the "[%]" specialization pattern, and the [with "[%]"]
+(** [FromPure] is used when introducing a pure assertion. It is used
+    by iPure, the "[%]" specialization pattern, and the [with "[%]"]
     pattern when using [iAssert].
 
     The [a] Boolean asserts whether we introduce the pure assertion in
     an affine way or in an absorbing way. When [FromPure true P φ] is
     derived, then [FromPure false P φ] can always be derived too. We
-    use [true] for specialization patterns and [false] for the [iPure]
-    tactic.
+    use [true] for specialization patterns and [false] for the
+    [iPureIntro] tactic.
 
     This Boolean is not needed for [IntoPure], because in the case of
     [IntoPure], we can have the same behavior by asking that [P] be
-- 
GitLab