aboutsummaryrefslogtreecommitdiffhomepage
path: root/library/nameops.ml
diff options
context:
space:
mode:
Diffstat (limited to 'library/nameops.ml')
-rw-r--r--library/nameops.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/library/nameops.ml b/library/nameops.ml
index 98b417c2a..71405d024 100644
--- a/library/nameops.ml
+++ b/library/nameops.ml
@@ -12,7 +12,7 @@ open Names
(* Identifiers *)
-let pr_id id = str (Id.to_string id)
+let pr_id id = Id.print id
let pr_name = function
| Anonymous -> str "_"
@@ -141,7 +141,7 @@ let name_max na1 na2 =
| Name _ -> na1
| Anonymous -> na2
-let pr_lab l = str (Label.to_string l)
+let pr_lab l = Label.print l
let default_library = Names.DirPath.initial (* = ["Top"] *)