diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-11-13 18:43:02 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-11-13 18:45:41 +0100 |
| commit | c571cdbbcac5cb4b4a5a19ab2f7ac51222316292 (patch) | |
| tree | 2ec7070bc8d58ee4b6fd0734ea41964243a0f2ba /vernac/classes.ml | |
| parent | 6bd240fce21c172680a0cec5346b66e08c76418a (diff) | |
[api] Another large deprecation, `Nameops`
Diffstat (limited to 'vernac/classes.ml')
| -rw-r--r-- | vernac/classes.ml | 2 |
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 |