From 67c713cab69a54f5347c987aa0076aeddd1bceef Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 16 Oct 2016 19:04:29 +0200
Subject: Fix bug #5141: Bogus message "Error: Cannot infer type of
 pattern-matching".

We simply explicit that the type is actually referring to the return type,
not to the type of the argument of the pattern-matching. Note that the
heuristic could be enhanced so as to use the same code in both let-style
and match-style pattern-matching, but I'm leaving this for another time.
---
 toplevel/himsg.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index 6ee695bc24..56b4779555 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -516,7 +516,8 @@ let explain_cant_find_case_type env sigma c =
   let c = Evarutil.nf_evar sigma c in
   let env = make_all_name_different env in
   let pe = pr_lconstr_env env sigma c in
-  str "Cannot infer type of pattern-matching on" ++ ws 1 ++ pe ++ str "."
+  str "Cannot infer the return type of pattern-matching on" ++ ws 1 ++
+    pe ++ str "."
 
 let explain_occur_check env sigma ev rhs =
   let rhs = Evarutil.nf_evar sigma rhs in
-- 
cgit v1.2.3