diff options
Diffstat (limited to 'tactics/declareUctx.ml')
| -rw-r--r-- | tactics/declareUctx.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/declareUctx.ml b/tactics/declareUctx.ml index bca43697cb..6c8bc92865 100644 --- a/tactics/declareUctx.ml +++ b/tactics/declareUctx.ml @@ -16,7 +16,7 @@ let name_instance inst = assert false | Some na -> try - let qid = Nametab.shortest_qualid_of_universe Names.Id.Set.empty na in + let qid = Nametab.shortest_qualid_of_universe Names.Id.Map.empty na in Names.Name (Libnames.qualid_basename qid) with Not_found -> (* Best-effort naming from the string representation of the level. |