diff options
Diffstat (limited to 'toplevel/autoinstance.ml')
| -rw-r--r-- | toplevel/autoinstance.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/toplevel/autoinstance.ml b/toplevel/autoinstance.ml index 29bef7b5a..4946ee933 100644 --- a/toplevel/autoinstance.ml +++ b/toplevel/autoinstance.ml @@ -161,7 +161,7 @@ let new_inst_no = fun () -> incr cnt; string_of_int !cnt let make_instance_ident gr = - Nameops.add_suffix (Nametab.id_of_global gr) ("_autoinstance_"^new_inst_no()) + Nameops.add_suffix (Nametab.basename_of_global gr) ("_autoinstance_"^new_inst_no()) let new_instance_message ident typ def = Flags.if_verbose |