From 68db732f12980e592c610085192d93457f312607 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 8 Feb 2016 11:19:09 +0100
Subject: Improving error message with missing patterns in the presence of
 multiple patterns.

---
 toplevel/himsg.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index 89c33cb6fe..c0a99fe75c 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -1207,7 +1207,7 @@ let explain_unused_clause env pats =
 let explain_non_exhaustive env pats =
   str "Non exhaustive pattern-matching: no clause found for " ++
   str (String.plural (List.length pats) "pattern") ++
-  spc () ++ hov 0 (pr_sequence pr_cases_pattern pats)
+  spc () ++ hov 0 (prlist_with_sep pr_comma pr_cases_pattern pats)
 
 let explain_cannot_infer_predicate env sigma typs =
   let env = make_all_name_different env in
-- 
cgit v1.2.3