diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2016-12-07 12:12:54 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-03-21 15:51:42 +0100 |
| commit | 3b3d5937939ac8dc4f152d61391630e62bb0b2e5 (patch) | |
| tree | 562c3470d8d2f02226ccf27d032a64a5e9a5dc17 /vernac/auto_ind_decl.ml | |
| parent | 3fc02bb2034a648c9c27b76a9e7b4e02a78e55b9 (diff) | |
[pp] [ide] Minor cleanups in pp code.
- We avoid unnecessary use of Pp -> string conversion functions.
and the creation of intermediate buffers on logging.
- We rename local functions that share the name with the Coq stdlib,
this is usually dangerous as if the normal function is removed, code
may pick up the one in the stdlib, with different semantics.
Diffstat (limited to 'vernac/auto_ind_decl.ml')
| -rw-r--r-- | vernac/auto_ind_decl.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml index 594f2e944..6d71601cc 100644 --- a/vernac/auto_ind_decl.ml +++ b/vernac/auto_ind_decl.ml @@ -444,14 +444,14 @@ let do_replace_bl mode bl_scheme_key (ind,u as indu) aavoid narg lft rgt = with Not_found -> (* spiwack: the format of this error message should probably be improved. *) - let err_msg = string_of_ppcmds + let err_msg = (str "boolean->Leibniz:" ++ str "You have to declare the" ++ str "decidability over " ++ Printer.pr_constr tt1 ++ str " first.") in - error err_msg + user_err err_msg in let bl_args = Array.append (Array.append (Array.map (fun x -> x) v) |