aboutsummaryrefslogtreecommitdiffhomepage
path: root/library/nametab.ml
diff options
context:
space:
mode:
Diffstat (limited to 'library/nametab.ml')
-rw-r--r--library/nametab.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/library/nametab.ml b/library/nametab.ml
index 40acb3ae2..bbae98fc0 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