aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel
diff options
context:
space:
mode:
Diffstat (limited to 'toplevel')
-rw-r--r--toplevel/himsg.ml3
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