From fe56bc97653123d24631b0f9ed2e100259202099 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Fri, 20 Nov 2020 10:14:21 +0100
Subject: [doc] [ssr] fix documentation of reflect

---
 theories/ssr/ssrbool.v | 9 +++++----
 1 file changed, 5 insertions(+), 4 deletions(-)

diff --git a/theories/ssr/ssrbool.v b/theories/ssr/ssrbool.v
index b205965ed1..d1cefeb552 100644
--- a/theories/ssr/ssrbool.v
+++ b/theories/ssr/ssrbool.v
@@ -22,9 +22,10 @@ Require Import ssreflect ssrfun.
                is_true b == the coercion of b : bool to Prop (:= b = true).
                             This is just input and displayed as `b''.
              reflect P b == the reflection inductive predicate, asserting
-                            that the logical proposition P : prop with the
-                            formula b : bool. Lemmas asserting reflect P b
-                            are often referred to as "views".
+                            that the logical proposition P : Prop holds iff
+                            the formula b : bool is equal to true. Lemmas
+                            asserting reflect P b are often referred to as
+                            "views".
   iffP, appP, sameP, rwP :: lemmas for direct manipulation of reflection
                             views: iffP is used to prove reflection from
                             logical equivalence, appP to compose views, and
@@ -33,7 +34,7 @@ Require Import ssreflect ssrfun.
                    elimT :: coercion reflect >-> Funclass, which allows the
                             direct application of `reflect' views to
                             boolean assertions.
-             decidable P <-> P is effectively decidable (:= {P} + {~ P}.
+             decidable P <-> P is effectively decidable (:= {P} + {~ P}).
     contra, contraL, ... :: contraposition lemmas.
            altP my_viewP :: natural alternative for reflection; given
                             lemma myviewP: reflect my_Prop my_formula,
-- 
cgit v1.2.3