From 0ec6fa02debadc832b03668d9031b03ee12a84e9 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 9 Jul 2014 19:19:35 -0700 Subject: [PATCH] feat(frontends/lean/pp_options): remove the 'lean.' prefix Signed-off-by: Leonardo de Moura --- src/frontends/lean/pp_options.cpp | 24 ++++++++++++------------ 1 file changed, 12 insertions(+), 12 deletions(-) diff --git a/src/frontends/lean/pp_options.cpp b/src/frontends/lean/pp_options.cpp index 4b53335eb7..23a4bf0ca2 100644 --- a/src/frontends/lean/pp_options.cpp +++ b/src/frontends/lean/pp_options.cpp @@ -31,25 +31,25 @@ Author: Leonardo de Moura #endif namespace lean { -static name g_pp_max_depth {"lean", "pp", "max_depth"}; -static name g_pp_max_steps {"lean", "pp", "max_steps"}; -static name g_pp_notation {"lean", "pp", "notation"}; -static name g_pp_implicit {"lean", "pp", "implicit"}; -static name g_pp_coercion {"lean", "pp", "coercion"}; -static name g_pp_universes {"lean", "pp", "universes"}; +static name g_pp_max_depth {"pp", "max_depth"}; +static name g_pp_max_steps {"pp", "max_steps"}; +static name g_pp_notation {"pp", "notation"}; +static name g_pp_implicit {"pp", "implicit"}; +static name g_pp_coercion {"pp", "coercion"}; +static name g_pp_universes {"pp", "universes"}; RegisterUnsignedOption(g_pp_max_depth, LEAN_DEFAULT_PP_MAX_DEPTH, - "(lean pretty printer) maximum expression depth, after that it will use ellipsis"); + "(pretty printer) maximum expression depth, after that it will use ellipsis"); RegisterUnsignedOption(g_pp_max_steps, LEAN_DEFAULT_PP_MAX_STEPS, - "(lean pretty printer) maximum number of visited expressions, after that it will use ellipsis"); + "(pretty printer) maximum number of visited expressions, after that it will use ellipsis"); RegisterBoolOption(g_pp_notation, LEAN_DEFAULT_PP_NOTATION, - "(lean pretty printer) disable/enable notation (infix, mixfix, postfix operators and unicode characters)"); + "(pretty printer) disable/enable notation (infix, mixfix, postfix operators and unicode characters)"); RegisterBoolOption(g_pp_implicit, LEAN_DEFAULT_PP_IMPLICIT, - "(lean pretty printer) display implicit parameters"); + "(pretty printer) display implicit parameters"); RegisterBoolOption(g_pp_coercion, LEAN_DEFAULT_PP_COERCION, - "(lean pretty printer) display coercions"); + "(pretty printer) display coercions"); RegisterBoolOption(g_pp_universes, LEAN_DEFAULT_PP_UNIVERSES, - "(lean pretty printer) display universes"); + "(pretty printer) display universes"); 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); }