diff options
| author | Pierre-Marie Pédrot | 2016-10-17 18:09:28 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-10-17 18:09:28 +0200 |
| commit | 1929b52db6bc282c60a1a3aa39ba87307c68bf78 (patch) | |
| tree | 57a6c7632dec646afb3ab6a1a9519eb313e805ac /toplevel | |
| parent | 05ad4f49ac2203dd64dfec79a1fc62ee52115724 (diff) | |
| parent | 34b1813b5adf1df556e0d8a05bde0ec58152f610 (diff) | |
Merge branch 'v8.6'
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/coqtop.ml | 6 | ||||
| -rw-r--r-- | toplevel/himsg.ml | 3 |
2 files changed, 4 insertions, 5 deletions
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index ebdf804ba0..7a67e0951f 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -61,8 +61,7 @@ let init_color () = match colors with | None -> (** Default colors *) - Ppstyle.init_color_output (); - Feedback.set_logger Feedback.color_terminal_logger + Feedback.init_color_output () | Some "" -> (** No color output *) () @@ -70,8 +69,7 @@ let init_color () = (** Overwrite all colors *) Ppstyle.clear_styles (); Ppstyle.parse_config s; - Ppstyle.init_color_output (); - Feedback.set_logger Feedback.color_terminal_logger + Feedback.init_color_output () end let toploop_init = ref begin fun x -> diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml index 66781a8c36..f7fafab495 100644 --- a/toplevel/himsg.ml +++ b/toplevel/himsg.ml @@ -515,7 +515,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 |