From 82a7de83cc338c6ad1262813c2bef76a819f9df0 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 25 Aug 2014 10:23:28 -0700 Subject: [PATCH] feat(frontends/lean/pp_options): use a more effective get_distinguishing_pp_options Signed-off-by: Leonardo de Moura --- src/frontends/lean/pp_options.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/frontends/lean/pp_options.cpp b/src/frontends/lean/pp_options.cpp index 271be287dd..b444be7119 100644 --- a/src/frontends/lean/pp_options.cpp +++ b/src/frontends/lean/pp_options.cpp @@ -64,7 +64,7 @@ list const & get_distinguishing_pp_options() { static options g_implicit_coercion = join(g_coercion_true, g_implicit_true); static options g_implicit_notation = join(g_notation_false, g_implicit_true); static options g_all = join(join(g_universes_true, g_implicit_true), join(g_coercion_true, g_notation_false)); - static list g_distinguishing_pp_options({g_universes_true, g_implicit_true, g_coercion_true, g_implicit_coercion, g_implicit_notation, g_all}); + static list g_distinguishing_pp_options({g_implicit_true, g_coercion_true, g_implicit_coercion, g_implicit_notation, g_universes_true, g_all}); return g_distinguishing_pp_options; }