diff options
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/auto_ind_decl.ml | 10 | ||||
| -rw-r--r-- | toplevel/ide_slave.ml | 4 |
2 files changed, 4 insertions, 10 deletions
diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml index 83b63067e..f4dab15f0 100644 --- a/toplevel/auto_ind_decl.ml +++ b/toplevel/auto_ind_decl.ml @@ -346,13 +346,12 @@ let do_replace_lb lb_scheme_key aavoid narg gls p q = with Not_found -> (* spiwack: the format of this error message should probably be improved. *) - let err_msg = msg_with Format.str_formatter + let err_msg = string_of_ppcmds (str "Leibniz->boolean:" ++ str "You have to declare the" ++ str "decidability over " ++ Printer.pr_constr type_of_pq ++ - str " first."); - Format.flush_str_formatter () + str " first.") in error err_msg in let lb_args = Array.append (Array.append @@ -404,13 +403,12 @@ let do_replace_bl bl_scheme_key ind gls aavoid narg lft rgt = with Not_found -> (* spiwack: the format of this error message should probably be improved. *) - let err_msg = msg_with Format.str_formatter + let err_msg = string_of_ppcmds (str "boolean->Leibniz:" ++ str "You have to declare the" ++ str "decidability over " ++ Printer.pr_constr tt1 ++ - str " first."); - Format.flush_str_formatter () + str " first.") in error err_msg in let bl_args = diff --git a/toplevel/ide_slave.ml b/toplevel/ide_slave.ml index cbd7d4353..5309a4505 100644 --- a/toplevel/ide_slave.ml +++ b/toplevel/ide_slave.ml @@ -352,10 +352,6 @@ let rewind count = (** Goal display *) -let string_of_ppcmds c = - Pp.msg_with Format.str_formatter c; - Format.flush_str_formatter () - let hyp_next_tac sigma env (id,_,ast) = let id_s = Names.string_of_id id in let type_s = string_of_ppcmds (pr_ltype_env env ast) in |