From c03ae24d2283a940a81fd4b4b830d69df8df853b Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 13 Jul 2014 14:03:47 +0100 Subject: [PATCH] fix(frontends/lean/elaborator): option name Signed-off-by: Leonardo de Moura --- src/frontends/lean/elaborator.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp index c6d46d6aa..3ca51be21 100644 --- a/src/frontends/lean/elaborator.cpp +++ b/src/frontends/lean/elaborator.cpp @@ -40,7 +40,7 @@ Author: Leonardo de Moura namespace lean { // ========================================== // elaborator configuration options -static name g_elaborator_local_instances{"lean", "elaborator", "local_instances"}; +static name g_elaborator_local_instances{"elaborator", "local_instances"}; RegisterBoolOption(g_elaborator_local_instances, LEAN_DEFAULT_ELABORATOR_LOCAL_INSTANCES, "(lean elaborator) use local declarates as class instances"); bool get_elaborator_local_instances(options const & opts) { return opts.get_bool(g_elaborator_local_instances, LEAN_DEFAULT_ELABORATOR_LOCAL_INSTANCES);