From 602badcad9deec9224b78cd1e1033af30358ef2e Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Tue, 22 Dec 2015 22:35:09 +0100 Subject: 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. --- library/nametab.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'library/nametab.ml') diff --git a/library/nametab.ml b/library/nametab.ml index 5b6d7cd98..621640ef9 100644 --- a/library/nametab.ml +++ b/library/nametab.ml @@ -523,7 +523,7 @@ let shortest_qualid_of_tactic kn = KnTab.shortest_qualid Id.Set.empty sp !the_tactictab let pr_global_env env ref = - try str (string_of_qualid (shortest_qualid_of_global env ref)) + try pr_qualid (shortest_qualid_of_global env ref) with Not_found as e -> if !Flags.debug then Pp.msg_debug (Pp.str "pr_global_env not found"); raise e -- cgit v1.2.3