From 9315f079d43e2895b9e04dbe5aafecddb1c78f59 Mon Sep 17 00:00:00 2001
From: Clément Blaudeau
Date: Tue, 8 Sep 2020 11:45:06 +0200
Subject: [Small typo] Update match.rst

Some error messages were merged together---
 doc/sphinx/language/extensions/match.rst | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'doc')

diff --git a/doc/sphinx/language/extensions/match.rst b/doc/sphinx/language/extensions/match.rst
index 34752a4c4d..e887ca8e98 100644
--- a/doc/sphinx/language/extensions/match.rst
+++ b/doc/sphinx/language/extensions/match.rst
@@ -880,10 +880,10 @@ Here is a summary of the error messages corresponding to each
 situation:
 
 .. exn:: The constructor @ident expects @num arguments.
+         The variable ident is bound several times in pattern term
+         Found a constructor of inductive type term while a constructor of term is expected
 
-   The variable ident is bound several times in pattern termFound a constructor
-   of inductive type term while a constructor of term is expectedPatterns are
-   incorrect (because constructors are not applied to the correct number of the
+   Patterns are incorrect (because constructors are not applied to the correct number of the
    arguments, because they are not linear or they are wrongly typed).
 
 .. exn:: Non exhaustive pattern matching.
-- 
cgit v1.2.3