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 | |
| 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')
| -rw-r--r-- | vernac/auto_ind_decl.ml | 4 | ||||
| -rw-r--r-- | vernac/vernacentries.ml | 4 |
2 files changed, 4 insertions, 4 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) diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 09c43f93e..999fe297e 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -39,7 +39,7 @@ module NamedDecl = Context.Named.Declaration let (f_interp_redexp, interp_redexp_hook) = Hook.make () let debug = false -let prerr_endline x = +let vernac_prerr_endline x = if debug then prerr_endline (x ()) else () (* Misc *) @@ -1933,7 +1933,7 @@ let vernac_load interp fname = * still parsed as the obsolete_locality grammar entry for retrocompatibility. * loc is the Loc.t of the vernacular command being interpreted. *) let interp ?proof ~loc locality poly c = - prerr_endline (fun () -> "interpreting: " ^ Pp.string_of_ppcmds (Ppvernac.pr_vernac c)); + vernac_prerr_endline (fun () -> "interpreting: " ^ Pp.string_of_ppcmds (Ppvernac.pr_vernac c)); match c with (* The below vernac are candidates for removal from the main type and to be put into a new doc_command datatype: *) |