michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

feat(frontends/lean/pp_options): use a more effective get_distinguishing_pp_options

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-08-25 10:23:28 -07:00
parent 42a8fb5965
commit 82a7de83cc
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/frontends/lean/pp_options.cpp
View file

@ -64,7 +64,7 @@ list<options> 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<options> g_distinguishing_pp_options({g_universes_true, g_implicit_true, g_coercion_true, g_implicit_coercion, g_implicit_notation, g_all});
static list<options> 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;
}