From a95c781dadd2b4aa5a6b715cfc7238e761a807fc Mon Sep 17 00:00:00 2001
From: Vincent Laporte
Date: Wed, 24 Oct 2018 11:09:01 +0000
Subject: [Manual] Fix layout of a list

---
 doc/sphinx/proof-engine/ssreflect-proof-language.rst | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

(limited to 'doc/sphinx/proof-engine')

diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
index 52609546d5..e976396950 100644
--- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst
+++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
@@ -3756,9 +3756,10 @@ which the function is supplied:
    :name: congr
 
 This tactic:
-+ checks that the goal is a Leibniz equality
-+ matches both sides of this equality with “term applied to some arguments”, inferring the right number of arguments from the goal and the type of term. This may expand some definitions or fixpoints.
-+ generates the subgoals corresponding to pairwise equalities of the arguments present in the goal.
+
+   + checks that the goal is a Leibniz equality;
+   + matches both sides of this equality with “term applied to some arguments”, inferring the right number of arguments from the goal and the type of term. This may expand some definitions or fixpoints;
+   + generates the subgoals corresponding to pairwise equalities of the arguments present in the goal.
 
 The goal can be a non dependent product ``P -> Q``. In that case, the
 system asserts the equation ``P = Q``, uses it to solve the goal, and
-- 
cgit v1.2.3