From ecb23dc8db0682ec327a110482b034677aecb6e9 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Wed, 2 Dec 2020 14:09:06 +0100
Subject: Stop calling Id.Map.domain on univ binders every individual universe

---
 tactics/declareUctx.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'tactics')

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.
-- 
cgit v1.2.3