From 41e14fddf8b2e69e4df7bac7b7ef4590e3f13057 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 10 Nov 2015 20:02:31 -0800
Subject: [PATCH] feat(library/head_map): support local name in the head_map

---
 src/library/head_map.cpp | 8 +++++---
 src/library/head_map.h   | 4 ++--
 2 files changed, 7 insertions(+), 5 deletions(-)

diff --git a/src/library/head_map.cpp b/src/library/head_map.cpp
index 7003677b9..af6944e10 100644
--- a/src/library/head_map.cpp
+++ b/src/library/head_map.cpp
@@ -22,13 +22,15 @@ head_index::head_index(expr const & e) {
     }
     m_kind = f.kind();
     if (is_constant(f))
-        m_const_name = const_name(f);
+        m_name = const_name(f);
+    else if (is_local(f))
+        m_name = mlocal_name(f);
 }
 
 int head_index::cmp::operator()(head_index const & i1, head_index const & i2) const {
-    if (i1.m_kind != i2.m_kind || i1.m_kind != expr_kind::Constant)
+    if (i1.m_kind != i2.m_kind || (i1.m_kind != expr_kind::Constant && i1.m_kind != expr_kind::Local))
         return static_cast<int>(i1.m_kind) - static_cast<int>(i2.m_kind);
     else
-        return quick_cmp(i1.m_const_name, i2.m_const_name);
+        return quick_cmp(i1.m_name, i2.m_name);
 }
 }
diff --git a/src/library/head_map.h b/src/library/head_map.h
index 18b0a96ac..4a9cc8037 100644
--- a/src/library/head_map.h
+++ b/src/library/head_map.h
@@ -12,9 +12,9 @@ Author: Leonardo de Moura
 namespace lean {
 struct head_index {
     expr_kind m_kind;
-    name      m_const_name;
+    name      m_name;
     explicit head_index(expr_kind k = expr_kind::Var):m_kind(k) {}
-    explicit head_index(name const & c):m_kind(expr_kind::Constant), m_const_name(c) {}
+    explicit head_index(name const & c):m_kind(expr_kind::Constant), m_name(c) {}
     head_index(expr const & e);
 
     struct cmp {