aboutsummaryrefslogtreecommitdiffhomepage
path: root/vernac/classes.ml
diff options
context:
space:
mode:
Diffstat (limited to 'vernac/classes.ml')
-rw-r--r--vernac/classes.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/vernac/classes.ml b/vernac/classes.ml
index 22117f7e1..20cb43b24 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -180,7 +180,7 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance)
Name id ->
let sp = Lib.make_path id in
if Nametab.exists_cci sp then
- user_err ~hdr:"new_instance" (Nameops.pr_id id ++ Pp.str " already exists.");
+ user_err ~hdr:"new_instance" (Id.print id ++ Pp.str " already exists.");
id
| Anonymous ->
let i = Nameops.add_suffix (id_of_class k) "_instance_0" in