From f344dd75c411ea21047568ee8479ceb201ea1e4f Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 8 Jan 2015 11:55:08 -0800
Subject: [PATCH] feat(library/pp_options): add get_pp_purify_locals_name

---
 src/library/pp_options.cpp | 1 +
 src/library/pp_options.h   | 1 +
 2 files changed, 2 insertions(+)

diff --git a/src/library/pp_options.cpp b/src/library/pp_options.cpp
index c876eedba..ca79adaf8 100644
--- a/src/library/pp_options.cpp
+++ b/src/library/pp_options.cpp
@@ -154,6 +154,7 @@ name const & get_pp_universes_option_name() { return *g_pp_universes; }
 name const & get_pp_notation_option_name() { return *g_pp_notation; }
 name const & get_pp_metavar_args_name() { return *g_pp_metavar_args; }
 name const & get_pp_purify_metavars_name() { return *g_pp_purify_metavars; }
+name const & get_pp_purify_locals_name() { return *g_pp_purify_locals; }
 
 unsigned get_pp_max_depth(options const & opts)       { return opts.get_unsigned(*g_pp_max_depth, LEAN_DEFAULT_PP_MAX_DEPTH); }
 unsigned get_pp_max_steps(options const & opts)       { return opts.get_unsigned(*g_pp_max_steps, LEAN_DEFAULT_PP_MAX_STEPS); }
diff --git a/src/library/pp_options.h b/src/library/pp_options.h
index a5f43e17f..3720a9bb4 100644
--- a/src/library/pp_options.h
+++ b/src/library/pp_options.h
@@ -14,6 +14,7 @@ name const & get_pp_universes_option_name();
 name const & get_pp_notation_option_name();
 name const & get_pp_metavar_args_name();
 name const & get_pp_purify_metavars_name();
+name const & get_pp_purify_locals_name();
 
 unsigned get_pp_max_depth(options const & opts);
 unsigned get_pp_max_steps(options const & opts);