aboutsummaryrefslogtreecommitdiffhomepage
path: root/printing/printmod.ml
diff options
context:
space:
mode:
authorGravatar Guillaume Melquiond <guillaume.melquiond@inria.fr>2015-12-22 22:35:09 +0100
committerGravatar Guillaume Melquiond <guillaume.melquiond@inria.fr>2015-12-22 22:35:09 +0100
commit602badcad9deec9224b78cd1e1033af30358ef2e (patch)
treee528188a52c4120fa94a5e0ff2c035874dee75cf /printing/printmod.ml
parentd55676344c8dc0d9a87b2ef12ec2348281db4bf5 (diff)
Do not compose "str" and "to_string" whenever possible.
For instance, calling only Id.print is faster than calling both str and Id.to_string, since the latter performs a copy. It also makes the code a bit simpler to read.
Diffstat (limited to 'printing/printmod.ml')
-rw-r--r--printing/printmod.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/printing/printmod.ml b/printing/printmod.ml
index d6f847cc7..e0b1d55be 100644
--- a/printing/printmod.ml
+++ b/printing/printmod.ml
@@ -264,7 +264,7 @@ let nametab_register_modparam mbid mtb =
List.iter (nametab_register_body mp dir) struc
let print_body is_impl env mp (l,body) =
- let name = str (Label.to_string l) in
+ let name = pr_label l in
hov 2 (match body with
| SFBmodule _ -> keyword "Module" ++ spc () ++ name
| SFBmodtype _ -> keyword "Module Type" ++ spc () ++ name