From f39f25519c89fb88388f8677e7e7f4664aaae7c9 Mon Sep 17 00:00:00 2001
From: Antonio Nikishaev
Date: Sun, 24 Nov 2019 19:26:02 +0400
Subject: fix «W -- weakening» doc

---
 plugins/ssr/ssrbool.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins')

diff --git a/plugins/ssr/ssrbool.v b/plugins/ssr/ssrbool.v
index 376410658a..f6b192c226 100644
--- a/plugins/ssr/ssrbool.v
+++ b/plugins/ssr/ssrbool.v
@@ -290,7 +290,7 @@ Require Import ssreflect ssrfun.
    r -- a right-hand operation, as orb_andr : rightt_distributive orb andb.
    T or t -- boolean truth, as in andbT: right_id true andb.
    U -- predicate union, as in predU.
-   W -- weakening, as in in1W : {in D, forall x, P} -> forall x, P.          **)
+   W -- weakening, as in in1W : (forall x, P) -> {in D, forall x, P}.        **)
 
 
 Set Implicit Arguments.
-- 
cgit v1.2.3