From e6fbbbbc2dcd83cf19e235023ba3a4813fdaf4ba Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 3 Oct 2016 16:26:58 -0700
Subject: [PATCH] feat(util/rb_map): add unsigned_map

---
 src/library/local_context.h      | 2 +-
 src/library/tactic/kabstract.cpp | 6 +++---
 src/util/rb_map.h                | 2 ++
 3 files changed, 6 insertions(+), 4 deletions(-)

diff --git a/src/library/local_context.h b/src/library/local_context.h
index dda4f669cf..178edcb30f 100644
--- a/src/library/local_context.h
+++ b/src/library/local_context.h
@@ -73,7 +73,7 @@ name mk_local_decl_name();
 class metavar_context;
 
 class local_context {
-    typedef rb_map<unsigned, local_decl, unsigned_cmp> idx2local_decl;
+    typedef unsigned_map<local_decl> idx2local_decl;
     unsigned                   m_next_idx;
     name_map<local_decl>       m_name2local_decl;
     subscripted_name_set  m_user_names;
diff --git a/src/library/tactic/kabstract.cpp b/src/library/tactic/kabstract.cpp
index 59eeab91ec..98e440a811 100644
--- a/src/library/tactic/kabstract.cpp
+++ b/src/library/tactic/kabstract.cpp
@@ -20,9 +20,9 @@ struct key_equivalence_ext : public environment_extension {
         unsigned m_rank;
     };
 
-    unsigned                             m_next_idx;
-    rb_map<unsigned, node, unsigned_cmp> m_nodes;
-    name_map<node_ref>                   m_to_node;
+    unsigned           m_next_idx;
+    unsigned_map<node> m_nodes;
+    name_map<node_ref> m_to_node;
 
     node_ref mk_node() {
         node_ref r = m_next_idx;
diff --git a/src/util/rb_map.h b/src/util/rb_map.h
index 07ec5fa639..b61edc057c 100644
--- a/src/util/rb_map.h
+++ b/src/util/rb_map.h
@@ -127,4 +127,6 @@ template<typename K, typename T, typename CMP, typename F>
 void for_each(rb_map<K, T, CMP> const & m, F && f) {
     return m.for_each(f);
 }
+
+template<typename T> using unsigned_map = rb_map<unsigned, T, unsigned_cmp>;
 }