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/vernacentries.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/vernacentries.ml')
| -rw-r--r-- | vernac/vernacentries.ml | 4 |
1 files changed, 2 insertions, 2 deletions
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: *) |