From 35a2d07115cb1b41c5a32f8abd3608e37eae32dc Mon Sep 17 00:00:00 2001
From: Vincent Laporte
Date: Wed, 24 Oct 2018 11:38:09 +0000
Subject: [Manual] Typo

---
 doc/sphinx/proof-engine/ssreflect-proof-language.rst | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
index 70d17b1915..4fc3c24e89 100644
--- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst
+++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
@@ -4920,7 +4920,7 @@ which produces the converse implication. In both cases, the two
 first Prop arguments are implicit.
 
 If ``term`` is an instance of the ``reflect`` predicate, then ``A`` will be one
-of the defined view hints for the ``reflec``t predicate, which are by
+of the defined view hints for the ``reflect`` predicate, which are by
 default the ones present in the file ``ssrbool.v``. These hints are not
 only used for choosing the appropriate direction of the translation,
 but they also allow complex transformation, involving negations.
-- 
cgit v1.2.3