diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-10-16 19:04:29 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-10-16 19:04:29 +0200 |
| commit | 67c713cab69a54f5347c987aa0076aeddd1bceef (patch) | |
| tree | 314a1e576d2abaf7765975f6c19651bd0cdec691 /toplevel | |
| parent | c3b9a7bf9fcd162628ce6a2a544652ca096cfe54 (diff) | |
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.
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/himsg.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml index 6ee695bc2..56b477955 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 |